src/Pure/Thy/thy_load.ML
author wenzelm
Mon Nov 02 20:50:48 2009 +0100 (2009-11-02)
changeset 33388 d64545e6cba5
parent 33221 5bb809208876
child 37216 3165bc303f66
permissions -rw-r--r--
modernized structure Proof_Syntax;
wenzelm@6168
     1
(*  Title:      Pure/Thy/thy_load.ML
wenzelm@6168
     2
    Author:     Markus Wenzel, TU Muenchen
wenzelm@6168
     3
wenzelm@15801
     4
Theory loader primitives, including load path.
wenzelm@6168
     5
*)
wenzelm@6168
     6
wenzelm@6168
     7
signature BASIC_THY_LOAD =
wenzelm@6168
     8
sig
wenzelm@6168
     9
  val show_path: unit -> string list
wenzelm@6168
    10
  val add_path: string -> unit
wenzelm@10252
    11
  val path_add: string -> unit
wenzelm@6168
    12
  val del_path: string -> unit
wenzelm@7438
    13
  val with_path: string -> ('a -> 'b) -> 'a -> 'b
wenzelm@9103
    14
  val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
wenzelm@6205
    15
  val reset_path: unit -> unit
wenzelm@6168
    16
end;
wenzelm@6168
    17
wenzelm@6168
    18
signature THY_LOAD =
wenzelm@6168
    19
sig
wenzelm@6168
    20
  include BASIC_THY_LOAD
wenzelm@17366
    21
  val ml_exts: string list
wenzelm@6205
    22
  val ml_path: string -> Path.T
wenzelm@7901
    23
  val thy_path: string -> Path.T
wenzelm@29418
    24
  val split_thy_path: Path.T -> Path.T * string
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@24189
    27
  val check_thy: Path.T -> string -> Path.T * File.ident
wenzelm@29515
    28
  val check_name: string -> string -> unit
wenzelm@24189
    29
  val deps_thy: Path.T -> string ->
wenzelm@24189
    30
   {master: Path.T * File.ident, text: string list, imports: string list, uses: Path.T list}
wenzelm@23885
    31
  val load_ml: Path.T -> Path.T -> Path.T * File.ident
wenzelm@6168
    32
end;
wenzelm@6168
    33
wenzelm@26616
    34
structure ThyLoad: THY_LOAD =
wenzelm@6168
    35
struct
wenzelm@6168
    36
wenzelm@6168
    37
wenzelm@6232
    38
(* maintain load path *)
wenzelm@6168
    39
wenzelm@32738
    40
local val load_path = Unsynchronized.ref [Path.current] in
wenzelm@6168
    41
wenzelm@21858
    42
fun show_path () = map Path.implode (! load_path);
wenzelm@23944
    43
wenzelm@33221
    44
fun del_path s =
wenzelm@33221
    45
  CRITICAL (fn () => Unsynchronized.change load_path (remove (op =) (Path.explode s)));
wenzelm@33221
    46
wenzelm@33221
    47
fun add_path s =
wenzelm@33221
    48
  CRITICAL (fn () => (del_path s; Unsynchronized.change load_path (cons (Path.explode s))));
wenzelm@33221
    49
wenzelm@33221
    50
fun path_add s =
wenzelm@33221
    51
  CRITICAL (fn () =>
wenzelm@32738
    52
    (del_path s; Unsynchronized.change load_path (fn path => path @ [Path.explode s])));
wenzelm@33221
    53
wenzelm@6205
    54
fun reset_path () = load_path := [Path.current];
wenzelm@23944
    55
wenzelm@23944
    56
fun with_paths ss f x =
wenzelm@33221
    57
  CRITICAL (fn () =>
wenzelm@33221
    58
    setmp_CRITICAL load_path (! load_path @ map Path.explode ss) f x);
wenzelm@33221
    59
wenzelm@9655
    60
fun with_path s f x = with_paths [s] f x;
wenzelm@6168
    61
wenzelm@23944
    62
fun search_path dir path =
wenzelm@23944
    63
  distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
wenzelm@23944
    64
wenzelm@23944
    65
end;
wenzelm@23944
    66
wenzelm@6168
    67
wenzelm@6232
    68
(* file formats *)
wenzelm@6168
    69
wenzelm@23872
    70
val ml_exts = ["ML", "sml"];
wenzelm@6232
    71
val ml_path = Path.ext "ML" o Path.basic;
wenzelm@6232
    72
val thy_path = Path.ext "thy" o Path.basic;
wenzelm@6168
    73
wenzelm@29418
    74
fun split_thy_path path =
wenzelm@29418
    75
  (case Path.split_ext path of
wenzelm@29418
    76
    (path', "thy") => (Path.dir path', Path.implode (Path.base path'))
wenzelm@29418
    77
  | _ => error ("Bad theory file specification " ^ Path.implode path));
wenzelm@29418
    78
wenzelm@6168
    79
wenzelm@23872
    80
(* check files *)
wenzelm@6232
    81
wenzelm@32811
    82
fun check_ext exts paths src_path =
wenzelm@6232
    83
  let
wenzelm@6232
    84
    val path = Path.expand src_path;
wenzelm@23872
    85
    val _ = Path.is_current path andalso error "Bad file specification";
wenzelm@6168
    86
wenzelm@23885
    87
    fun try_ext rel_path ext =
wenzelm@8750
    88
      let val ext_path = Path.expand (Path.ext ext rel_path)
wenzelm@23872
    89
      in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
wenzelm@23885
    90
    fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
wenzelm@23944
    91
  in get_first try_prfx paths end;
wenzelm@6232
    92
wenzelm@32811
    93
fun check_file dir path = check_ext [] (search_path dir path) path;
wenzelm@32811
    94
fun check_ml dir path = check_ext ml_exts (search_path dir path) path;
wenzelm@6168
    95
wenzelm@24189
    96
fun check_thy dir name =
wenzelm@23944
    97
  let
wenzelm@23944
    98
    val thy_file = thy_path name;
wenzelm@23944
    99
    val paths = search_path dir thy_file;
wenzelm@23944
   100
  in
wenzelm@32811
   101
    (case check_ext [] paths thy_file of
wenzelm@23872
   102
      NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
wenzelm@23944
   103
        " in " ^ commas_quote (map Path.implode paths))
wenzelm@24189
   104
    | SOME thy_id => thy_id)
wenzelm@23872
   105
  end;
wenzelm@6232
   106
wenzelm@29515
   107
fun check_name name name' =
wenzelm@29515
   108
  if name = name' then ()
wenzelm@29515
   109
  else error ("Filename " ^ quote (Path.implode (thy_path name)) ^
wenzelm@29515
   110
    " does not agree with theory name " ^ quote name');
wenzelm@29515
   111
wenzelm@6232
   112
wenzelm@23872
   113
(* theory deps *)
wenzelm@7940
   114
wenzelm@24189
   115
fun deps_thy dir name =
wenzelm@23872
   116
  let
wenzelm@24189
   117
    val master as (path, _) = check_thy dir name;
wenzelm@24065
   118
    val text = explode (File.read path);
wenzelm@23872
   119
    val (name', imports, uses) =
wenzelm@32466
   120
      Thy_Header.read (Path.position path) (Source.of_list_limited 8000 text);
wenzelm@29515
   121
    val _ = check_name name name';
wenzelm@24189
   122
    val uses = map (Path.explode o #1) uses;
wenzelm@24065
   123
  in {master = master, text = text, imports = imports, uses = uses} end;
wenzelm@6484
   124
wenzelm@6168
   125
wenzelm@23872
   126
(* load files *)
wenzelm@6168
   127
wenzelm@23885
   128
fun load_ml dir raw_path =
wenzelm@23885
   129
  (case check_ml dir raw_path of
wenzelm@23872
   130
    NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
wenzelm@26455
   131
  | SOME (path, id) => (ML_Context.eval_file path; (path, id)));
wenzelm@6168
   132
wenzelm@6168
   133
end;
wenzelm@6168
   134
wenzelm@32738
   135
structure Basic_Thy_Load: BASIC_THY_LOAD = ThyLoad;
wenzelm@32738
   136
open Basic_Thy_Load;