src/Pure/Thy/thy_load.ML
author wenzelm
Mon Jul 23 16:45:03 2007 +0200 (2007-07-23)
changeset 23935 2a4e42ec9a54
parent 23892 739707039b0d
child 23944 2ea068548a83
permissions -rw-r--r--
PrintMode.with_modes;
     1 (*  Title:      Pure/Thy/thy_load.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 Theory loader primitives, including load path.
     6 *)
     7 
     8 signature BASIC_THY_LOAD =
     9 sig
    10   val show_path: unit -> string list
    11   val add_path: string -> unit
    12   val path_add: 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 ml_exts: string list
    23   val ml_path: string -> Path.T
    24   val thy_path: string -> Path.T
    25   val check_file: Path.T -> Path.T -> (Path.T * File.ident) option
    26   val check_ml: Path.T -> Path.T -> (Path.T * File.ident) option
    27   val check_thy: Path.T -> string -> bool -> (Path.T * File.ident) * (Path.T * File.ident) option
    28   val deps_thy: Path.T -> string -> bool ->
    29     ((Path.T * File.ident) * (Path.T * File.ident) option) * (string list * Path.T list)
    30   val load_ml: Path.T -> Path.T -> Path.T * File.ident
    31   val load_thy: Path.T -> string -> bool -> bool ->
    32     (Path.T * File.ident) * (Path.T * File.ident) option
    33 end;
    34 
    35 (*this backdoor sealed later*)
    36 signature PRIVATE_THY_LOAD =
    37 sig
    38   include THY_LOAD
    39   val load_thy_fn: (Path.T -> string -> bool -> bool ->
    40     (Path.T * File.ident) * (Path.T * File.ident) option) ref
    41 end;
    42 
    43 structure ThyLoad: PRIVATE_THY_LOAD =
    44 struct
    45 
    46 
    47 (* maintain load path *)
    48 
    49 val load_path = ref [Path.current];
    50 
    51 fun show_path () = map Path.implode (! load_path);
    52 fun del_path s = change load_path (remove (op =) (Path.explode s));
    53 fun add_path s = (del_path s; change load_path (cons (Path.explode s)));
    54 fun path_add s = (del_path s; change load_path (fn path => path @ [Path.explode s]));
    55 fun reset_path () = load_path := [Path.current];
    56 fun with_paths ss f x = Library.setmp load_path (! load_path @ map Path.explode ss) f x;
    57 fun with_path s f x = with_paths [s] f x;
    58 
    59 
    60 (* file formats *)
    61 
    62 val ml_exts = ["ML", "sml"];
    63 val ml_path = Path.ext "ML" o Path.basic;
    64 val thy_path = Path.ext "thy" o Path.basic;
    65 
    66 
    67 (* check files *)
    68 
    69 fun search_path dir path =
    70   distinct (op =) (dir :: (if Path.is_basic path then (! load_path) else [Path.current]));
    71 
    72 fun check_ext exts dir src_path =
    73   let
    74     val path = Path.expand src_path;
    75     val _ = Path.is_current path andalso error "Bad file specification";
    76 
    77     fun try_ext rel_path ext =
    78       let val ext_path = Path.expand (Path.ext ext rel_path)
    79       in Option.map (fn id => (File.full_path ext_path, id)) (File.ident ext_path) end;
    80     fun try_prfx prfx = get_first (try_ext (Path.append prfx path)) ("" :: exts);
    81   in get_first try_prfx (search_path dir path) end;
    82 
    83 val check_file = check_ext [];
    84 val check_ml = check_ext ml_exts;
    85 
    86 fun check_thy dir name ml =
    87   let val thy_file = thy_path name in
    88     (case check_file dir thy_file of
    89       NONE => error ("Could not find theory file " ^ quote (Path.implode thy_file) ^
    90         " in " ^ commas_quote (map Path.implode (search_path dir thy_file)))
    91     | SOME thy_id => (thy_id, if ml then check_file dir (ml_path name) else NONE))
    92   end;
    93 
    94 
    95 (* theory deps *)
    96 
    97 fun deps_thy dir name ml =
    98   let
    99     val master as ((path, _), _) = check_thy dir name ml;
   100     val (name', imports, uses) =
   101       ThyHeader.read (Position.path path) (Source.of_string_limited (File.read path));
   102     val _ = name = name' orelse
   103       error ("Filename " ^ quote (Path.implode (Path.base path)) ^
   104         " does not agree with theory name " ^ quote name');
   105     val ml_file =
   106       if ml andalso is_some (check_file dir (ml_path name))
   107       then [ml_path name] else [];
   108   in (master, (imports, map (Path.explode o #1) uses @ ml_file)) end;
   109 
   110 
   111 (* load files *)
   112 
   113 fun load_ml dir raw_path =
   114   (case check_ml dir raw_path of
   115     NONE => error ("Could not find ML file " ^ quote (Path.implode raw_path))
   116   | SOME (path, id) => (ML_Context.use path; (path, id)));
   117 
   118 (*dependent on outer syntax*)
   119 val load_thy_fn = ref (undefined: Path.T -> string -> bool -> bool ->
   120   (Path.T * File.ident) * (Path.T * File.ident) option);
   121 fun load_thy dir name ml time = ! load_thy_fn dir name ml time;
   122 
   123 end;
   124 
   125 structure BasicThyLoad: BASIC_THY_LOAD = ThyLoad;
   126 open BasicThyLoad;