diff --git a/Makefile.in b/Makefile.in
index b312b4940db6733fb2305adfcbf6c6a24d8cebd6..87d5fe4c5e5f3dae851ea81d98add0c561bc738b 100644
--- a/Makefile.in
+++ b/Makefile.in
@@ -390,12 +390,12 @@ $(PGMCMO) $(PGMCMX): INCLUDES += -I src/programs
byte: bin/why3ml.byte
opt: bin/why3ml.opt
-bin/why3ml.opt: src/why3.cmxa $(PGMCMX) src/main.cmx
+bin/why3ml.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) src/main.cmx
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
-bin/why3ml.byte: src/why3.cma $(PGMCMO) src/main.cmo
+bin/why3ml.byte: src/why3.cma $(PGMCMO) $(MLWCMO) src/main.cmo
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
@@ -573,12 +573,12 @@ bin/why3ide.opt bin/why3ide.byte: INCLUDES += -I @LABLGTK2LIB@
bin/why3ide.opt bin/why3ide.byte: EXTOBJS +=
bin/why3ide.opt bin/why3ide.byte: EXTLIBS += lablgtk lablgtksourceview2
-bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(IDECMX)
+bin/why3ide.opt: src/why3.cmxa $(PGMCMX) $(MLWCMX) $(IDECMX)
$(if $(QUIET), @echo 'Linking $@' &&) \
$(OCAMLOPT) $(OFLAGS) -o $@ $(EXTCMXA) $^
$(STRIP) $@
-bin/why3ide.byte: src/why3.cma $(PGMCMO) $(IDECMO)
+bin/why3ide.byte: src/why3.cma $(PGMCMO) $(MLWCMO) $(IDECMO)
$(if $(QUIET),@echo 'Linking $@' &&) \
$(OCAMLC) $(BFLAGS) -o $@ $(EXTCMA) $^
diff --git a/src/core/env.ml b/src/core/env.ml
index c05a1ea8e67e75c98bde35a872ec15d8a6f7ac86..63c3f089ae7bf394e21da69edec54878873b7d52 100644
--- a/src/core/env.ml
+++ b/src/core/env.ml
@@ -179,8 +179,6 @@ let read_lib_theory lib path th =
try Mstr.find th mth with Not_found ->
raise (TheoryNotFound (path,th))
-let read_lib_file lib path = fst (read_lib_file lib path)
-
let register_format name exts read =
if Hashtbl.mem read_format_table name then raise (KnownFormat name);
let getlib = Wenv.memoize 5 (mk_library read exts) in
diff --git a/src/core/env.mli b/src/core/env.mli
index f51eb93f9ae2bbed4c97d785934785885e941cf9..86371cd5c9e4998ceb53026c02a2fb7478578100 100644
--- a/src/core/env.mli
+++ b/src/core/env.mli
@@ -114,7 +114,7 @@ val env_of_library : 'a library -> env
val list_formats : unit -> (fformat * extension list) list
(** [list_formats ()] returns the list of registered formats *)
-val read_lib_file : 'a library -> pathname -> 'a
+val read_lib_file : 'a library -> pathname -> 'a * theory Mstr.t
(** [read_lib_file lib path] retrieves the contents of a library file
@raise LibFileNotFound [path] if the library file was not found *)
diff --git a/src/core/theory.ml b/src/core/theory.ml
index de7cbf7aafa7d0b928fbdd78083e2cf2dce359c4..a0cf52910da19ca57473a1ad79c7eef6a11d16d6 100644
--- a/src/core/theory.ml
+++ b/src/core/theory.ml
@@ -663,7 +663,6 @@ let is_empty_sm sm =
Mls.is_empty sm.sm_ls &&
Mpr.is_empty sm.sm_pr
-
(** Meta properties *)
let get_meta_arg_type = function
diff --git a/src/core/theory.mli b/src/core/theory.mli
index 0328fbcc170f88d4a45f09da14f3d3a83f03d471..6a0f4202fcabb0ac3c18d46337f7ae7275ca39f7 100644
--- a/src/core/theory.mli
+++ b/src/core/theory.mli
@@ -124,6 +124,7 @@ val close_theory : theory_uc -> theory
val open_namespace : theory_uc -> theory_uc
val close_namespace : theory_uc -> bool -> string option -> theory_uc
+ (* the Boolean indicates [import]; the string option indicates [as T] *)
val get_namespace : theory_uc -> namespace
val get_known : theory_uc -> known_map
diff --git a/src/parser/parser.mly b/src/parser/parser.mly
index e06389e5458c84d035425178489736580423691a..8fc923868370dd6ba84e9ec2beda6a084ca27b46 100644
--- a/src/parser/parser.mly
+++ b/src/parser/parser.mly
@@ -62,6 +62,7 @@ module Incremental = struct
let new_use_clone d =
let env = ref_get env_ref in let lenv = ref_get lenv_ref in
ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) d)
+
end
open Ptree
@@ -184,6 +185,9 @@ end
| Term.IConstBinary s -> int_of_string ("0b"^s)
with Failure _ -> raise Parsing.Parse_error
+ let qualid_last = function
+ | Qident x | Qdot (_, x) -> x.id
+
%}
/* Tokens */
@@ -316,7 +320,7 @@ namespace_import:
;
namespace_name:
-| uident { Some $1 }
+| uident { Some $1.id }
| UNDERSCORE { None }
;
@@ -354,17 +358,17 @@ use_clone:
use:
| imp_exp tqualid
- { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
+ { { use_theory = $2; use_as = Some (qualid_last $2); use_imp_exp = $1 } }
| imp_exp tqualid AS uident
- { { use_theory = $2; use_as = Some (Some $4); use_imp_exp = $1 } }
+ { { use_theory = $2; use_as = Some $4.id; use_imp_exp = $1 } }
| imp_exp tqualid AS UNDERSCORE
- { { use_theory = $2; use_as = Some None; use_imp_exp = $1 } }
+ { { use_theory = $2; use_as = None; use_imp_exp = $1 } }
;
imp_exp:
-| IMPORT { Import }
-| EXPORT { Export }
-| /* epsilon */ { Nothing }
+| IMPORT { Some true }
+| EXPORT { None }
+| /* epsilon */ { Some false }
;
clone_subst:
@@ -378,13 +382,13 @@ list1_comma_subst:
;
subst:
-| NAMESPACE ns EQUAL ns { CSns ($2, $4) }
-| TYPE qualid EQUAL qualid { CStsym ($2, $4) }
-| CONSTANT qualid EQUAL qualid { CSfsym ($2, $4) }
-| FUNCTION qualid EQUAL qualid { CSfsym ($2, $4) }
-| PREDICATE qualid EQUAL qualid { CSpsym ($2, $4) }
-| LEMMA qualid { CSlemma $2 }
-| GOAL qualid { CSgoal $2 }
+| NAMESPACE ns EQUAL ns { CSns (floc (), $2, $4) }
+| TYPE qualid EQUAL qualid { CStsym (floc (), $2, $4) }
+| CONSTANT qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
+| FUNCTION qualid EQUAL qualid { CSfsym (floc (), $2, $4) }
+| PREDICATE qualid EQUAL qualid { CSpsym (floc (), $2, $4) }
+| LEMMA qualid { CSlemma (floc (), $2) }
+| GOAL qualid { CSgoal (floc (), $2) }
;
ns:
@@ -1062,9 +1066,9 @@ opt_semicolon:
use_module:
| imp_exp MODULE tqualid
- { Duse ($3, $1, None) }
+ { Duse ($3, $1, Some (qualid_last $3)) }
| imp_exp MODULE tqualid AS uident
- { Duse ($3, $1, Some $5) }
+ { Duse ($3, $1, Some $5.id) }
;
list1_recfun_sep_and:
diff --git a/src/parser/ptree.ml b/src/parser/ptree.ml
index 09a03cfb1c010626d5af0d774183c491898c7d5a..102905ab51138afe7e0820df8d41dc40802fbd60 100644
--- a/src/parser/ptree.ml
+++ b/src/parser/ptree.ml
@@ -94,22 +94,21 @@ type plogic_type =
| PPredicate of pty list
| PFunction of pty list * pty
-type imp_exp =
- | Import | Export | Nothing
-
type use = {
use_theory : qualid;
- use_as : ident option option;
- use_imp_exp : imp_exp;
+ use_as : string option;
+ (* None = as _, Some id = as id *)
+ use_imp_exp : bool option;
+ (* None = export, Some false = default, Some true = import *)
}
type clone_subst =
- | CSns of qualid option * qualid option
- | CStsym of qualid * qualid
- | CSfsym of qualid * qualid
- | CSpsym of qualid * qualid
- | CSlemma of qualid
- | CSgoal of qualid
+ | CSns of loc * qualid option * qualid option
+ | CStsym of loc * qualid * qualid
+ | CSfsym of loc * qualid * qualid
+ | CSpsym of loc * qualid * qualid
+ | CSlemma of loc * qualid
+ | CSgoal of loc * qualid
type is_mutable = bool
@@ -246,8 +245,8 @@ type program_decl =
| Dparam of ident * type_v
| Dexn of ident * pty option
(* modules *)
- | Duse of qualid * imp_exp * (*as:*) ident option
- | Dnamespace of loc * ident option * (* import: *) bool * program_decl list
+ | Duse of qualid * bool option * (*as:*) string option
+ | Dnamespace of loc * string option * (* import: *) bool * program_decl list
type theory = {
pth_name : ident;
diff --git a/src/parser/typing.ml b/src/parser/typing.ml
index 5ddc1b07454fc0fea59bbf16096d8211e0296bd4..572d940b3ab24e787ea8fd71edf81b31e546d4e8 100644
--- a/src/parser/typing.ml
+++ b/src/parser/typing.ml
@@ -31,7 +31,6 @@ open Denv
(** errors *)
-exception Message of string
exception DuplicateTypeVar of string
exception TypeArity of qualid * int * int
exception Clash of string
@@ -47,28 +46,15 @@ exception UnboundTypeVar of string
exception UnboundType of string list
exception UnboundSymbol of string list
-let error ?loc e = match loc with
- | None -> raise e
- | Some loc -> raise (Loc.Located (loc,e))
-
-let errorm ?loc f =
- let buf = Buffer.create 512 in
- let fmt = Format.formatter_of_buffer buf in
- Format.kfprintf
- (fun _ ->
- Format.pp_print_flush fmt ();
- let s = Buffer.contents buf in
- Buffer.clear buf;
- error ?loc (Message s))
- fmt f
+let error = Loc.error
+
+let errorm = Loc.errorm
let rec print_qualid fmt = function
| Qident s -> fprintf fmt "%s" s.id
| Qdot (m, s) -> fprintf fmt "%a.%s" print_qualid m s.id
let () = Exn_printer.register (fun fmt e -> match e with
- | Message s ->
- fprintf fmt "%s" s
| DuplicateTypeVar s ->
fprintf fmt "duplicate type parameter %s" s
| TypeArity (id, a, n) ->
@@ -1135,6 +1121,44 @@ let add_decl th = function
let add_decl th d =
if Debug.test_flag debug_parse_only then th else add_decl th d
+let type_inst th t s =
+ let add_inst s = function
+ | CSns (loc,p,q) ->
+ let find ns x = find_namespace_ns x ns in
+ let ns1 = option_fold find t.th_export p in
+ let ns2 = option_fold find (get_namespace th) q in
+ clone_ns loc t.th_local ns2 ns1 s
+ | CStsym (loc,p,q) ->
+ let ts1 = find_tysymbol_ns p t.th_export in
+ let ts2 = find_tysymbol q th in
+ if Mts.mem ts1 s.inst_ts
+ then error ~loc (Clash ts1.ts_name.id_string);
+ { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
+ | CSfsym (loc,p,q) ->
+ let ls1 = find_fsymbol_ns p t.th_export in
+ let ls2 = find_fsymbol q th in
+ if Mls.mem ls1 s.inst_ls
+ then error ~loc (Clash ls1.ls_name.id_string);
+ { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
+ | CSpsym (loc,p,q) ->
+ let ls1 = find_psymbol_ns p t.th_export in
+ let ls2 = find_psymbol q th in
+ if Mls.mem ls1 s.inst_ls
+ then error ~loc (Clash ls1.ls_name.id_string);
+ { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
+ | CSlemma (loc,p) ->
+ let pr = find_prop_ns p t.th_export in
+ if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
+ then error ~loc (Clash pr.pr_name.id_string);
+ { s with inst_lemma = Spr.add pr s.inst_lemma }
+ | CSgoal (loc,p) ->
+ let pr = find_prop_ns p t.th_export in
+ if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
+ then error ~loc (Clash pr.pr_name.id_string);
+ { s with inst_goal = Spr.add pr s.inst_goal }
+ in
+ List.fold_left add_inst empty_inst s
+
let add_use_clone env lenv th (loc, use, subst) =
if Debug.test_flag debug_parse_only then th else
let q, id = split_qualid use.use_theory in
@@ -1145,65 +1169,17 @@ let add_use_clone env lenv th (loc, use, subst) =
| TheoryNotFound _ -> error ~loc (UnboundTheory use.use_theory)
in
let use_or_clone th = match subst with
- | None ->
- use_export th t
- | Some s ->
- let add_inst s = function
- | CSns (p,q) ->
- let find ns x = find_namespace_ns x ns in
- let ns1 = option_fold find t.th_export p in
- let ns2 = option_fold find (get_namespace th) q in
- clone_ns loc t.th_local ns2 ns1 s
- | CStsym (p,q) ->
- let ts1 = find_tysymbol_ns p t.th_export in
- let ts2 = find_tysymbol q th in
- if Mts.mem ts1 s.inst_ts
- then error ~loc (Clash ts1.ts_name.id_string);
- { s with inst_ts = Mts.add ts1 ts2 s.inst_ts }
- | CSfsym (p,q) ->
- let ls1 = find_fsymbol_ns p t.th_export in
- let ls2 = find_fsymbol q th in
- if Mls.mem ls1 s.inst_ls
- then error ~loc (Clash ls1.ls_name.id_string);
- { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
- | CSpsym (p,q) ->
- let ls1 = find_psymbol_ns p t.th_export in
- let ls2 = find_psymbol q th in
- if Mls.mem ls1 s.inst_ls
- then error ~loc (Clash ls1.ls_name.id_string);
- { s with inst_ls = Mls.add ls1 ls2 s.inst_ls }
- | CSlemma p ->
- let pr = find_prop_ns p t.th_export in
- if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
- then error ~loc (Clash pr.pr_name.id_string);
- { s with inst_lemma = Spr.add pr s.inst_lemma }
- | CSgoal p ->
- let pr = find_prop_ns p t.th_export in
- if Spr.mem pr s.inst_lemma || Spr.mem pr s.inst_goal
- then error ~loc (Clash pr.pr_name.id_string);
- { s with inst_goal = Spr.add pr s.inst_goal }
- in
- let s = List.fold_left add_inst empty_inst s in
- clone_export th t s
- in
- let n = match use.use_as with
- | None -> Some t.th_name.id_string
- | Some (Some x) -> Some x.id
- | Some None -> None
+ | None -> use_export th t
+ | Some s -> clone_export th t (type_inst th t s)
in
begin try match use.use_imp_exp with
- | Nothing ->
- (* use T = namespace T use_export T end *)
- let th = open_namespace th in
- let th = use_or_clone th in
- close_namespace th false n
- | Import ->
- (* use import T = namespace T use_export T end import T *)
- let th = open_namespace th in
- let th = use_or_clone th in
- close_namespace th true n
- | Export ->
- use_or_clone th
+ | Some imp ->
+ (* use T = namespace T use_export T end *)
+ let th = open_namespace th in
+ let th = use_or_clone th in
+ close_namespace th imp use.use_as
+ | None ->
+ use_or_clone th
with ClashSymbol s -> error ~loc (Clash s)
end
@@ -1214,13 +1190,12 @@ let close_theory loc lenv th =
if Mstr.mem id lenv then error ~loc (ClashTheory id);
Mstr.add id th lenv
-let close_namespace loc import name th =
- let id = option_map (fun id -> id.id) name in
+let close_namespace loc import id th =
try close_namespace th import id
with ClashSymbol s -> error ~loc (Clash s)
(*
Local Variables:
-compile-command: "unset LANG; make -C ../.. test"
+compile-command: "unset LANG; make -C ../.."
End:
*)
diff --git a/src/parser/typing.mli b/src/parser/typing.mli
index 773404733fa59fb1802c41ca1aef747de008427a..4cf4d90f5bf55e71028ea83174b9da46d39e63d0 100644
--- a/src/parser/typing.mli
+++ b/src/parser/typing.mli
@@ -35,7 +35,7 @@ val add_use_clone :
unit Env.library -> theory Mstr.t -> theory_uc -> Ptree.use_clone -> theory_uc
val close_namespace :
- Loc.position -> bool -> Ptree.ident option -> theory_uc -> theory_uc
+ Loc.position -> bool -> string option -> theory_uc -> theory_uc
val close_theory : Loc.position -> theory Mstr.t -> theory_uc -> theory Mstr.t
@@ -95,3 +95,4 @@ val list_fields: theory_uc ->
(** check that the given fields all belong to the same record type
and do not appear several times *)
+val type_inst: theory_uc -> theory -> Ptree.clone_subst list -> th_inst
diff --git a/src/programs/pgm_typing.ml b/src/programs/pgm_typing.ml
index 33ef5704187ac294ec9c47d03a4a465cfc83502b..ab3fef54fdaadef0fd504dba65e88a1c3d80a894 100644
--- a/src/programs/pgm_typing.ml
+++ b/src/programs/pgm_typing.ml
@@ -2262,7 +2262,7 @@ let find_module penv lmod q id = match q with
Mstr.find id lmod
| _ :: _ ->
(* module in file f *)
- Mstr.find id (Env.read_lib_file penv q)
+ Mstr.find id (fst (Env.read_lib_file penv q))
(* env = to retrieve theories and modules from the loadpath
lmod = local modules *)
@@ -2346,22 +2346,13 @@ let rec decl ~wp env ltm lmod uc = function
with Not_found ->
errorm ~loc "@[unbound module %a@]" print_qualid qid
in
- let n = match use_as with
- | None -> Some (m.m_name.id_string)
- | Some x -> Some x.id
- in
begin try match imp_exp with
- | Nothing ->
+ | Some imp ->
(* use T = namespace T use_export T end *)
let uc = open_namespace uc in
let uc = use_export uc m in
- close_namespace uc false n
- | Import ->
- (* use import T = namespace T use_export T end import T *)
- let uc = open_namespace uc in
- let uc = use_export uc m in
- close_namespace uc true n
- | Export ->
+ close_namespace uc imp use_as
+ | None ->
use_export uc m
with ClashSymbol s ->
errorm ~loc "clash with previous symbol %s" s
@@ -2369,7 +2360,6 @@ let rec decl ~wp env ltm lmod uc = function
| Ptree.Dnamespace (loc, id, import, dl) ->
let uc = open_namespace uc in
let uc = List.fold_left (decl ~wp env ltm lmod) uc dl in
- let id = option_map (fun id -> id.id) id in
begin try close_namespace uc import id
with ClashSymbol s -> errorm ~loc "clash with previous symbol %s" s end
| Ptree.Dlogic (TypeDecl d) ->
diff --git a/src/util/exn_printer.mli b/src/util/exn_printer.mli
index ce5fb7353a894dac02817abc75c520e79da2e65f..39adba7a7026740e2f65c0ffc47258e03fe56952 100644
--- a/src/util/exn_printer.mli
+++ b/src/util/exn_printer.mli
@@ -26,5 +26,5 @@ val register : exn_printer -> unit
(* Register a formatter of exception *)
val exn_printer : exn_printer
-(* exn_printer fmt exn : print the exception using all the previously
- registered printer and return *)
+(* [exn_printer fmt exn] prints exception [exn] using all previously
+ registered printers and returns *)
diff --git a/src/util/loc.ml b/src/util/loc.ml
index fa2d2665d38a416ba3c490e6304bc8c27cc74ad0..1b3fdd96f1984e4c66c40574131296840c36ae8c 100644
--- a/src/util/loc.ml
+++ b/src/util/loc.ml
@@ -54,8 +54,6 @@ let user_position fname lnum cnum1 cnum2 = (fname,lnum,cnum1,cnum2)
let get loc = loc
-exception Located of position * exn
-
let dummy_position = ("",0,0,0)
let join (f1,l1,b1,e1) (f2,_,b2,e2) =
@@ -77,9 +75,44 @@ let gen_report_position fmt (f,l,b,e) =
let report_position fmt = fprintf fmt "%a:@\n" gen_report_position
+(* located exceptions *)
+
+exception Located of position * exn
+
+let try1 loc f x =
+ try f x with Located _ as e -> raise e | e -> raise (Located (loc, e))
+let try2 loc f x y =
+ try f x y with Located _ as e -> raise e | e -> raise (Located (loc, e))
+let try3 loc f x y z =
+ try f x y z with Located _ as e -> raise e | e -> raise (Located (loc, e))
+let try4 loc f x y z t =
+ try f x y z t with Located _ as e -> raise e | e -> raise (Located (loc, e))
+
+let error ?loc e = match loc with
+ | None -> raise e
+ | Some loc -> raise (Located (loc, e))
+
+(* located messages *)
+
+exception Message of string
+
+let errorm ?loc f =
+ let buf = Buffer.create 512 in
+ let fmt = Format.formatter_of_buffer buf in
+ Format.kfprintf
+ (fun _ ->
+ Format.pp_print_flush fmt ();
+ let s = Buffer.contents buf in
+ Buffer.clear buf;
+ error ?loc (Message s))
+ fmt f
+
let () = Exn_printer.register
(fun fmt exn -> match exn with
| Located (loc,e) ->
fprintf fmt "%a%a" report_position loc Exn_printer.exn_printer e
- | _ -> raise exn)
+ | Message s ->
+ fprintf fmt "%s" s
+ | _ ->
+ raise exn)
diff --git a/src/util/loc.mli b/src/util/loc.mli
index 1b9f35a4fca80ea88e71c936cfd42e9d7e1786a9..dabe4715317ffdb36244fab973632110708952af 100644
--- a/src/util/loc.mli
+++ b/src/util/loc.mli
@@ -34,8 +34,6 @@ type position
val extract : Lexing.position * Lexing.position -> position
val join : position -> position -> position
-exception Located of position * exn
-
val dummy_position : position
val user_position : string -> int -> int -> int -> position
@@ -50,3 +48,19 @@ val gen_report_position : formatter -> position -> unit
val report_position : formatter -> position -> unit
+(* located exceptions *)
+
+exception Located of position * exn
+
+val try1: position -> ('a -> 'b) -> 'a -> 'b
+val try2: position -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'c
+val try3: position -> ('a -> 'b -> 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
+val try4: position -> ('a -> 'b -> 'c -> 'd -> 'e) -> 'a -> 'b -> 'c -> 'd -> 'e
+
+val error: ?loc:position -> exn -> 'a
+
+(* messages *)
+
+exception Message of string
+
+val errorm: ?loc:position -> ('a, Format.formatter, unit, 'b) format4 -> 'a
diff --git a/src/whyml/mlw_typing.ml b/src/whyml/mlw_typing.ml
index 6288bb5dab4635c17dae4cc61b23b7617385c4b1..7434c011d89754b8f3461ea6e318df05988cb79d 100644
--- a/src/whyml/mlw_typing.ml
+++ b/src/whyml/mlw_typing.ml
@@ -19,6 +19,7 @@
open Why3
open Util
+open Ident
open Theory
open Env
open Ptree
@@ -28,23 +29,94 @@ type mlw_contents = modul Mstr.t
type mlw_library = mlw_contents library
type mlw_file = mlw_contents * Theory.theory Mstr.t
- (* let type_only = Debug.test_flag Typing.debug_type_only in *)
+(* TODO: let type_only = Debug.test_flag Typing.debug_type_only in *)
-let add_theory _lib path mt m =
+let find_theory loc lib path s =
+ (* search first in .mlw files (using lib) *)
+ let thm =
+ try Some (Env.read_lib_theory lib path s)
+ with LibFileNotFound _ | TheoryNotFound _ -> None
+ in
+ (* search also in .why files *)
+ let th =
+ try Some (Env.find_theory (Env.env_of_library lib) path s)
+ with LibFileNotFound _ | TheoryNotFound _ -> None
+ in
+ match thm, th with
+ | Some _, Some _ ->
+ Loc.errorm ~loc
+ "a module/theory %s is defined both in Why and WhyML libraries" s
+ | None, None -> Loc.error ~loc (Env.TheoryNotFound (path, s))
+ | None, Some t | Some t, None -> t
+
+let find_theory loc lib mt path s = match path with
+ | [] -> (* local theory *)
+ begin try Mstr.find s mt with Not_found -> find_theory loc lib [] s end
+ | _ :: _ -> (* theory in file path *)
+ find_theory loc lib path s
+
+type theory_or_module = Theory of Theory.theory | Module of modul
+
+let find_module loc lib path s =
+ (* search first in .mlw files *)
+ let m, thm =
+ try
+ let mm, mt = Env.read_lib_file lib path in
+ Mstr.find_option s mm, Mstr.find_option s mt
+ with
+ | LibFileNotFound _ -> None, None
+ in
+ (* search also in .why files *)
+ let th =
+ try Some (Env.find_theory (Env.env_of_library lib) path s)
+ with LibFileNotFound _ | TheoryNotFound _ -> None
+ in
+ match m, thm, th with
+ | Some _, None, _ -> assert false
+ | _, Some _, Some _ ->
+ Loc.errorm ~loc
+ "a module/theory %s is defined both in Why and WhyML libraries" s
+ | None, None, None -> Loc.error ~loc (Env.TheoryNotFound (path, s))
+ | Some m, Some _, None -> Module m
+ | None, Some t, None | None, None, Some t -> Theory t
+
+let find_module loc lib mt mm path s = match path with
+ | [] -> (* local module/theory *)
+ begin try Module (Mstr.find s mm)
+ with Not_found -> begin try Theory (Mstr.find s mt)
+ with Not_found -> find_module loc lib [] s end end
+ | _ :: _ -> (* module/theory in file path *)
+ find_module loc lib path s
+
+let add_theory lib path mt m =
let id = m.pth_name in
let loc = id.id_loc in
let uc = Theory.create_theory ~path (Denv.create_user_id id) in
let rec add_decl uc = function
- | Duseclone (_loc, _use, None) (* use *) ->
- assert false (*TODO*)
- | Duseclone (_loc, _use, Some _s) (* clone *) ->
- assert false (*TODO*)
+ | Duseclone (loc, use, inst) ->
+ let path, s = Typing.split_qualid use.use_theory in
+ let th = find_theory loc lib mt path s in
+ (* open namespace, if any *)
+ let uc =
+ if use.use_imp_exp <> None then Theory.open_namespace uc else uc in
+ (* use or clone *)
+ let uc = match inst with
+ | None -> Theory.use_export uc th
+ | Some inst ->
+ let inst = Typing.type_inst uc th inst in
+ Theory.clone_export uc th inst
+ in
+ (* close namespace, if any *)
+ begin match use.use_imp_exp with
+ | None -> uc
+ | Some imp -> Theory.close_namespace uc imp use.use_as
+ end
| Dlogic d ->
Typing.add_decl uc d
| Dnamespace (loc, name, import, dl) ->
let uc = Theory.open_namespace uc in
let uc = List.fold_left add_decl uc dl in
- Typing.close_namespace loc import name uc
+ Loc.try3 loc Theory.close_namespace uc import name
| Dlet _ | Dletrec _ | Dparam _ | Dexn _ | Duse _ ->
assert false
in
diff --git a/tests/test-pgm-jcf.mlx b/tests/test-pgm-jcf.mlx
new file mode 100644
index 0000000000000000000000000000000000000000..479850aee6c6009e13e44fdd735c736a329eeaf1
--- /dev/null
+++ b/tests/test-pgm-jcf.mlx
@@ -0,0 +1,11 @@
+
+theory T
+ type t = int
+ goal G : forall x: t. x=0
+end
+
+(*
+Local Variables:
+compile-command: "unset LANG; ../bin/why3ide test-pgm-jcf.mlx"
+End:
+*)