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