src/Pure/Thy/thy_load.ML
author wenzelm
Wed Jun 21 20:38:25 2000 +0200 (2000-06-21)
changeset 9103 ef56f093259d
parent 8808 204f4ebbba64
child 9655 a4d2da014ec3
permissions -rw-r--r--
added with_paths;
     1 (*  Title:      Pure/Thy/thy_load.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4     License:    GPL (GNU GENERAL PUBLIC LICENSE)
     5 
     6 Theory loader primitives.
     7 *)
     8 
     9 signature BASIC_THY_LOAD =
    10 sig
    11   val show_path: unit -> string list
    12   val add_path: string -> unit
    13   val del_path: string -> unit
    14   val with_path: string -> ('a -> 'b) -> 'a -> 'b
    15   val with_paths: string list -> ('a -> 'b) -> 'a -> 'b
    16   val reset_path: unit -> unit
    17 end;
    18 
    19 signature THY_LOAD =
    20 sig
    21   include BASIC_THY_LOAD
    22   val cond_with_path: Path.T -> ('a -> 'b) -> 'a -> 'b
    23   val ml_path: string -> Path.T
    24   val thy_path: string -> Path.T
    25   val check_file: Path.T -> (Path.T * File.info) option
    26   val load_file: Path.T -> (Path.T * File.info)
    27   eqtype master
    28   val get_thy: master -> Path.T * File.info
    29   val check_thy: Path.T -> string -> bool -> master
    30   val deps_thy: Path.T -> string -> bool -> master * (string list * Path.T list)
    31   val load_thy: Path.T -> string -> bool -> bool -> master
    32 end;
    33 
    34 (*this backdoor sealed later*)
    35 signature PRIVATE_THY_LOAD =
    36 sig
    37   include THY_LOAD
    38   val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
    39   val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
    40 end;
    41 
    42 structure ThyLoad: PRIVATE_THY_LOAD =
    43 struct
    44 
    45 
    46 (* maintain load path *)
    47 
    48 val load_path = ref [Path.current];
    49 fun change_path f = load_path := f (! load_path);
    50 
    51 fun show_path () = map Path.pack (! load_path);
    52 fun add_path s = change_path (cons (Path.unpack s));
    53 fun del_path s = change_path (filter_out (equal (Path.unpack s)));
    54 fun reset_path () = load_path := [Path.current];
    55 fun with_path s f x = Library.setmp load_path (Path.unpack s :: ! load_path) f x;
    56 fun with_paths ss f x = Library.setmp load_path (map Path.unpack ss @ ! load_path) f x;
    57 
    58 fun cond_with_path path f x =
    59   if Path.is_current path then f x else Library.setmp load_path (path :: ! load_path) f x;
    60 
    61 
    62 (* file formats *)
    63 
    64 val ml_exts = ["", "ML", "sml"];
    65 val ml_path = Path.ext "ML" o Path.basic;
    66 val thy_path = Path.ext "thy" o Path.basic;
    67 
    68 
    69 (* check_file *)
    70 
    71 fun check_file src_path =
    72   let
    73     val path = Path.expand src_path;
    74 
    75     fun find_ext rel_path ext =
    76       let val ext_path = Path.expand (Path.ext ext rel_path)
    77       in apsome (fn info => (File.full_path ext_path, info)) (File.info ext_path) end;
    78 
    79     fun find_dir dir =
    80       get_first (find_ext (Path.append dir path)) ml_exts;
    81   in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
    82 
    83 
    84 (* load_file *)
    85 
    86 fun load_file raw_path =
    87   (case check_file raw_path of
    88     None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
    89   | Some (path, info) => (File.symbol_use path; (path, info)));
    90 
    91 
    92 (* datatype master *)
    93 
    94 datatype master = Master of (Path.T * File.info) * (Path.T * File.info) option;
    95 
    96 fun get_thy (Master (thy, _)) = thy;
    97 
    98 
    99 (* check / process theory files *)
   100 
   101 local
   102 
   103 fun check_thy_aux (name, ml) =
   104   (case check_file (thy_path name) of
   105     None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
   106       commas_quote (show_path ()))
   107   | Some thy_info => (thy_info, if ml then check_file (ml_path name) else None));
   108 
   109 in
   110 
   111 fun check_thy dir name ml = Master (cond_with_path dir check_thy_aux (name, ml));
   112 
   113 fun process_thy dir f name ml =
   114   let val master as Master ((path, _), _) = check_thy dir name ml
   115   in (master, cond_with_path dir f path) end;
   116 
   117 end;
   118 
   119 
   120 (* deps_thy and load_thy *)
   121 
   122 (*hooks for theory syntax dependent operations*)
   123 fun undefined _ = raise Match;
   124 val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
   125 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
   126 
   127 fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
   128 fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
   129 
   130 
   131 end;
   132 
   133 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
   134 open BasicThyLoad;