Commit 2f74fca2 authored by Andrei Paskevich's avatar Andrei Paskevich

Env: export base_language_builtin, needed for Pmodule.convert

parent 3a3d0d09
......@@ -52,7 +52,7 @@ type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a
type format_info = fformat * extension list * Pp.formatted
module Hpath = Hashtbl.Make(struct
module Hpath = Exthtbl.Make(struct
type t = pathname
let hash = Hashtbl.hash
let equal = (=)
......@@ -229,7 +229,7 @@ let read_theory env path s =
open Ident
open Theory
let base_builtin path =
let base_language_builtin =
let builtin s =
if s = builtin_theory.th_name.id_string then builtin_theory else
if s = highord_theory.th_name.id_string then highord_theory else
......@@ -238,11 +238,11 @@ let base_builtin path =
| Some n -> tuple_theory n
| None -> raise Not_found
in
match path with
| [s] -> Mstr.singleton s (builtin s)
| _ -> raise Not_found
Hpath.memo 7 (function
| [s] -> Mstr.singleton s (builtin s)
| _ -> raise Not_found)
let () = add_builtin base_language base_builtin
let () = add_builtin base_language base_language_builtin
(* Exception reporting *)
......
......@@ -69,6 +69,12 @@ val add_builtin : 'a language -> (pathname -> 'a) -> unit
[convert]'ed into exactly the same singleton [theory Mstr.t] maps
as stored for the base language. *)
val base_language_builtin : pathname -> Theory.theory Mstr.t
(** [base_language_builtin path] returns the builtin theories defined
by the base language. Any offspring language that provides extended
definitions of builtin theories must use these as the result of
the conversion function. *)
type 'a format_parser = env -> pathname -> filename -> in_channel -> 'a
(** [(fn : 'a format_parser) env path file ch] parses the in_channel [ch]
and returns the language-specific contents of type ['a]. References
......
......@@ -302,21 +302,26 @@ let add_pdecl ~vc uc d =
type mlw_file = pmodule Mstr.t
let convert =
let dummy_env = Env.create_env [] in
let convert mm = Mstr.map (fun m -> m.mod_theory) mm in
fun mm -> if Mstr.is_empty mm then Mstr.empty else
match (snd (Mstr.choose mm)).mod_theory.th_path with
| ("why3" :: _) as path ->
begin try Env.read_library Env.base_language dummy_env path
with Env.LibraryNotFound _ -> convert mm end
| _ -> convert mm
let convert mm =
let convert m = m.mod_theory in
if Mstr.is_empty mm then Mstr.empty else
match (snd (Mstr.choose mm)).mod_theory.th_path with
| "why3" :: path ->
begin try Env.base_language_builtin path
with Not_found -> Mstr.map convert mm end
| _ -> Mstr.map convert mm
let mlw_language = Env.register_language Env.base_language convert
open Theory
let () =
module Hpath = Exthtbl.Make(struct
type t = Env.pathname
let hash = Hashtbl.hash
let equal = (=)
end)
let mlw_language_builtin =
let builtin s =
if s = unit_module.mod_theory.th_name.id_string then unit_module else
if s = builtin_theory.th_name.id_string then builtin_module else
......@@ -325,10 +330,12 @@ let () =
match tuple_theory_name s with
| Some n -> tuple_module n
| None -> raise Not_found in
Env.add_builtin mlw_language (function
Hpath.memo 7 (function
| [s] -> Mstr.singleton s (builtin s)
| _ -> raise Not_found)
let () = Env.add_builtin mlw_language mlw_language_builtin
exception ModuleNotFound of Env.pathname * string
let read_module env path s =
......
......@@ -114,6 +114,8 @@ type mlw_file = pmodule Mstr.t
val mlw_language : mlw_file language
val mlw_language_builtin : pathname -> mlw_file
exception ModuleNotFound of pathname * string
val read_module : env -> pathname -> string -> pmodule
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment