Theory loader primitives.
authorwenzelm
Sat Jan 30 10:42:40 1999 +0100 (1999-01-30 ago)
changeset 61689d5b74068bf9
parent 6167 2f354020efc3
child 6169 f3f2560fbed9
Theory loader primitives.
src/Pure/Thy/thy_load.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/Thy/thy_load.ML	Sat Jan 30 10:42:40 1999 +0100
     1.3 @@ -0,0 +1,93 @@
     1.4 +(*  Title:      Pure/Thy/thy_load.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Markus Wenzel, TU Muenchen
     1.7 +
     1.8 +Theory loader primitives.
     1.9 +*)
    1.10 +
    1.11 +signature BASIC_THY_LOAD =
    1.12 +sig
    1.13 +  val show_path: unit -> string list
    1.14 +  val add_path: string -> unit
    1.15 +  val del_path: string -> unit
    1.16 +end;
    1.17 +
    1.18 +signature THY_LOAD =
    1.19 +sig
    1.20 +  include BASIC_THY_LOAD
    1.21 +  val thy_ext: string
    1.22 +  val find_file: Path.T -> (Path.T * File.info) option
    1.23 +  val check_file: Path.T -> File.info option
    1.24 +  val load_file: Path.T -> File.info
    1.25 +  val check_thy: string -> File.info
    1.26 +  val deps_thy: string -> File.info * (string list * Path.T list)
    1.27 +  val load_thy: string -> File.info * theory
    1.28 +end;
    1.29 +
    1.30 +signature PRIVATE_THY_LOAD =
    1.31 +sig
    1.32 +  include THY_LOAD
    1.33 +  val deps_thy_fn: (Path.T -> string list * Path.T list) ref
    1.34 +  val load_thy_fn: (Path.T -> theory) ref
    1.35 +end;
    1.36 +
    1.37 +structure ThyLoad: PRIVATE_THY_LOAD =
    1.38 +struct
    1.39 +
    1.40 +
    1.41 +(* load path *)
    1.42 +
    1.43 +val load_path = ref [Path.current];
    1.44 +fun change_path f = load_path := f (! load_path);
    1.45 +
    1.46 +fun show_path () = map Path.pack (! load_path);
    1.47 +fun add_path s = change_path (fn path => path @ [Path.unpack s]);
    1.48 +fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    1.49 +
    1.50 +
    1.51 +(* find / check file *)
    1.52 +
    1.53 +fun find_file file_src =
    1.54 +  let
    1.55 +    val file = Path.expand file_src;
    1.56 +    fun find dir =
    1.57 +      let val full_path = Path.append dir file
    1.58 +      in apsome (pair full_path) (File.info full_path) end;
    1.59 +  in get_first find (if Path.is_basic file then ! load_path else [Path.current]) end;
    1.60 +
    1.61 +
    1.62 +(* process ML files *)
    1.63 +
    1.64 +val check_file = apsome #2 o find_file;
    1.65 +
    1.66 +fun load_file raw_path =
    1.67 +  (case find_file raw_path of
    1.68 +    Some (path, info) => (Use.use_path path; info)
    1.69 +  | None => error ("Could not find ML file " ^ quote (Path.pack raw_path)));
    1.70 +
    1.71 +
    1.72 +(* process theory files *)
    1.73 +
    1.74 +val thy_ext = "thy";
    1.75 +
    1.76 +fun process_thy f name =
    1.77 +  let val path = Path.ext thy_ext (Path.basic name) in
    1.78 +    (case find_file path of
    1.79 +      Some (path, info) => (info, f path)
    1.80 +    | None => error ("Could not find theory file " ^ quote (Path.pack path)))
    1.81 +  end;
    1.82 +
    1.83 +(*hooks for theory syntax dependent operations*)
    1.84 +fun undefined _ = raise Match;
    1.85 +val deps_thy_fn = ref (undefined: Path.T -> string list * Path.T list);
    1.86 +val load_thy_fn = ref (undefined: Path.T -> theory);
    1.87 +
    1.88 +val check_thy = #1 o process_thy (K ());
    1.89 +val deps_thy = process_thy (fn path => ! deps_thy_fn path);
    1.90 +val load_thy = process_thy (fn path => ! load_thy_fn path);
    1.91 +
    1.92 +
    1.93 +end;
    1.94 +
    1.95 +structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
    1.96 +open BasicThyLoad;