src/Pure/Thy/thy_load.ML
author wenzelm
Sat Jan 30 10:42:40 1999 +0100 (1999-01-30 ago)
changeset 6168 9d5b74068bf9
child 6205 dd3d3da0f458
permissions -rw-r--r--
Theory loader primitives.
     1 (*  Title:      Pure/Thy/thy_load.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Theory loader primitives.
     6 *)
     7 
     8 signature BASIC_THY_LOAD =
     9 sig
    10   val show_path: unit -> string list
    11   val add_path: string -> unit
    12   val del_path: string -> unit
    13 end;
    14 
    15 signature THY_LOAD =
    16 sig
    17   include BASIC_THY_LOAD
    18   val thy_ext: string
    19   val find_file: Path.T -> (Path.T * File.info) option
    20   val check_file: Path.T -> File.info option
    21   val load_file: Path.T -> File.info
    22   val check_thy: string -> File.info
    23   val deps_thy: string -> File.info * (string list * Path.T list)
    24   val load_thy: string -> File.info * theory
    25 end;
    26 
    27 signature PRIVATE_THY_LOAD =
    28 sig
    29   include THY_LOAD
    30   val deps_thy_fn: (Path.T -> string list * Path.T list) ref
    31   val load_thy_fn: (Path.T -> theory) ref
    32 end;
    33 
    34 structure ThyLoad: PRIVATE_THY_LOAD =
    35 struct
    36 
    37 
    38 (* load path *)
    39 
    40 val load_path = ref [Path.current];
    41 fun change_path f = load_path := f (! load_path);
    42 
    43 fun show_path () = map Path.pack (! load_path);
    44 fun add_path s = change_path (fn path => path @ [Path.unpack s]);
    45 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    46 
    47 
    48 (* find / check file *)
    49 
    50 fun find_file file_src =
    51   let
    52     val file = Path.expand file_src;
    53     fun find dir =
    54       let val full_path = Path.append dir file
    55       in apsome (pair full_path) (File.info full_path) end;
    56   in get_first find (if Path.is_basic file then ! load_path else [Path.current]) end;
    57 
    58 
    59 (* process ML files *)
    60 
    61 val check_file = apsome #2 o find_file;
    62 
    63 fun load_file raw_path =
    64   (case find_file raw_path of
    65     Some (path, info) => (Use.use_path path; info)
    66   | None => error ("Could not find ML file " ^ quote (Path.pack raw_path)));
    67 
    68 
    69 (* process theory files *)
    70 
    71 val thy_ext = "thy";
    72 
    73 fun process_thy f name =
    74   let val path = Path.ext thy_ext (Path.basic name) in
    75     (case find_file path of
    76       Some (path, info) => (info, f path)
    77     | None => error ("Could not find theory file " ^ quote (Path.pack path)))
    78   end;
    79 
    80 (*hooks for theory syntax dependent operations*)
    81 fun undefined _ = raise Match;
    82 val deps_thy_fn = ref (undefined: Path.T -> string list * Path.T list);
    83 val load_thy_fn = ref (undefined: Path.T -> theory);
    84 
    85 val check_thy = #1 o process_thy (K ());
    86 val deps_thy = process_thy (fn path => ! deps_thy_fn path);
    87 val load_thy = process_thy (fn path => ! load_thy_fn path);
    88 
    89 
    90 end;
    91 
    92 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
    93 open BasicThyLoad;