Skip to content

GitLab

why3
why3
Commit e59abf8f authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

Mlw: rename Mdecl and Wmodule to avoid name clashes

parent dfd0187f
Hide whitespace changes
Inline Side-by-side
Showing with 132 additions and 127 deletions
Makefile.in
View file @ e59abf8f
......@@ -152,7 +152,7 @@ LIB_DRIVER = call_provers driver_ast driver_parser driver_lexer driver \
whyconf autodetection \
parse_smtv2_model_parser parse_smtv2_model_lexer parse_smtv2_model
LIB_MLW = ity expr dexpr mdecl wmodule
LIB_MLW = ity expr dexpr pdecl pmodule
LIB_PARSER = ptree glob parser typing lexer
......
src/mlw/mdecl.ml → src/mlw/pdecl.ml
View file @ e59abf8f
......@@ -142,21 +142,21 @@ let create_rec_variant_decl s cl =
(** {2 Module declarations} *)
type mdecl = {
md_node : mdecl_node;
md_pure : Decl.decl list;
md_syms : Sid.t;
md_news : Sid.t;
md_tag : int;
type pdecl = {
pd_node : pdecl_node;
pd_pure : Decl.decl list;
pd_syms : Sid.t;
pd_news : Sid.t;
pd_tag : int;
}
and mdecl_node =
| MDtype of its_defn list
| MDlet of let_defn
| MDexn of xsymbol
| MDpure
and pdecl_node =
| PDtype of its_defn list
| PDlet of let_defn
| PDexn of xsymbol
| PDpure
let md_equal : mdecl -> mdecl -> bool = (==)
let pd_equal : pdecl -> pdecl -> bool = (==)
let get_news node pure =
let news_id s id = Sid.add_new (Decl.ClashIdent id) id s in
......@@ -164,19 +164,19 @@ let get_news node pure =
let news_pure news d = Sid.union news d.Decl.d_news in
let news = List.fold_left news_pure Sid.empty pure in
match node with
| MDtype dl ->
| PDtype dl ->
let news_itd news d =
let news = news_id news d.itd_its.its_ts.ts_name in
let news = List.fold_left news_rs news d.itd_fields in
List.fold_left news_rs news d.itd_constructors in
List.fold_left news_itd news dl
| MDlet (LDvar (v,_)) -> news_id news v.pv_vs.vs_name
| MDlet (LDsym (s,_)) -> news_id news s.rs_name
| MDlet (LDrec rdl) ->
| PDlet (LDvar (v,_)) -> news_id news v.pv_vs.vs_name
| PDlet (LDsym (s,_)) -> news_id news s.rs_name
| PDlet (LDrec rdl) ->
let news_rd news d = news_id news d.rec_sym.rs_name in
List.fold_left news_rd news rdl
| MDexn xs -> news_id news xs.xs_name
| MDpure -> news
| PDexn xs -> news_id news xs.xs_name
| PDpure -> news
let get_syms node pure =
let syms_ts s ts = Sid.add ts.ts_name s in
......@@ -269,7 +269,7 @@ let get_syms node pure =
Sid.union syms (List.fold_left del_rd dsms rdl)
in
match node with
| MDtype dl ->
| PDtype dl ->
let syms_itd syms d =
(* the syms of the invariants are already in [pure] *)
let syms = Opt.fold syms_ity syms d.itd_its.its_def in
......@@ -278,7 +278,7 @@ let get_syms node pure =
let syms = List.fold_left add_fd syms d.itd_fields in
List.fold_left add_cs syms d.itd_constructors in
List.fold_left syms_itd syms dl
| MDlet ld ->
| PDlet ld ->
let syms = syms_let_defn syms ld in
let vars = match ld with
| LDvar (_,e) -> e.e_effect.eff_reads
......@@ -286,62 +286,67 @@ let get_syms node pure =
| LDrec rdl -> List.fold_left (fun s rd ->
Spv.union s (cty_reads rd.rec_fun.c_cty)) Spv.empty rdl in
Spv.fold (fun v s -> Sid.add v.pv_vs.vs_name s) vars syms
| MDexn xs -> syms_ity syms xs.xs_ity
| MDpure -> syms
| PDexn xs -> syms_ity syms xs.xs_ity
| PDpure -> syms
let mk_decl = let r = ref 0 in fun node pure ->
{ md_node = node; md_pure = pure;
md_syms = get_syms node pure;
md_news = get_news node pure;
md_tag = (incr r; !r) }
{ pd_node = node; pd_pure = pure;
pd_syms = get_syms node pure;
pd_news = get_news node pure;
pd_tag = (incr r; !r) }
let create_type_decl dl =
let ldl = assert false (* TODO *) in
mk_decl (MDtype dl) ldl
mk_decl (PDtype dl) ldl
let create_let_decl ld = let _ = MDlet ld in assert false (* TODO *)
let create_let_decl ld = let _ = PDlet ld in assert false (* TODO *)
let create_exn_decl xs = let _ = MDexn xs in assert false (* TODO *)
let create_exn_decl xs =
if not (ity_closed xs.xs_ity) then Loc.errorm ?loc:xs.xs_name.id_loc
"Top-level exception %a has a polymorphic type" print_xs xs;
if not xs.xs_ity.ity_pure then Loc.errorm ?loc:xs.xs_name.id_loc
"The type of top-level exception %a has mutable components" print_xs xs;
mk_decl (PDexn xs) []
let create_pure_decl _d = let _ = MDpure in assert false (* TODO *)
let create_pure_decl d = mk_decl PDpure [d]
(** {2 Built-in decls} *)
let md_int = mk_decl (MDtype [mk_itd its_int [] [] []]) [(*TODO*)]
let md_real = mk_decl (MDtype [mk_itd its_real [] [] []]) [(*TODO*)]
let md_unit = mk_decl (MDtype [mk_itd its_unit [] [] []]) [(*TODO*)]
let md_func = mk_decl (MDtype [mk_itd its_func [] [] []]) [(*TODO*)]
let md_pred = mk_decl (MDtype [mk_itd its_pred [] [] []]) [(*TODO*)]
let pd_int = mk_decl (PDtype [mk_itd its_int [] [] []]) [(*TODO*)]
let pd_real = mk_decl (PDtype [mk_itd its_real [] [] []]) [(*TODO*)]
let pd_unit = mk_decl (PDtype [mk_itd its_unit [] [] []]) [(*TODO*)]
let pd_func = mk_decl (PDtype [mk_itd its_func [] [] []]) [(*TODO*)]
let pd_pred = mk_decl (PDtype [mk_itd its_pred [] [] []]) [(*TODO*)]
let md_equ = mk_decl MDpure [(*TODO*)]
let pd_equ = mk_decl PDpure [(*TODO*)]
let md_bool =
mk_decl (MDtype [mk_itd its_bool [] [rs_true;rs_false] []]) [(*TODO*)]
let pd_bool =
mk_decl (PDtype [mk_itd its_bool [] [rs_true; rs_false] []]) [(*TODO*)]
let md_tuple _n = assert false (*TODO*)
let pd_tuple _n = assert false (*TODO*)
let md_func_app = mk_decl (MDlet ld_func_app) [(*TODO*)]
let pd_func_app = mk_decl (PDlet ld_func_app) [(*TODO*)]
(** {2 Known identifiers} *)
type known_map = mdecl Mid.t
type known_map = pdecl Mid.t
let known_id kn id =
if not (Mid.mem id kn) then raise (Decl.UnknownIdent id)
let merge_known kn1 kn2 =
let check_known id decl1 decl2 =
if md_equal decl1 decl2 then Some decl1
if pd_equal decl1 decl2 then Some decl1
else raise (Decl.RedeclaredIdent id) in
Mid.union check_known kn1 kn2
let known_add_decl kn0 d =
let kn = Mid.map (Util.const d) d.md_news in
let kn = Mid.map (Util.const d) d.pd_news in
let check id decl0 _ =
if md_equal decl0 d
if pd_equal decl0 d
then raise (Decl.KnownIdent id)
else raise (Decl.RedeclaredIdent id) in
let kn = Mid.union check kn0 kn in
let unk = Mid.set_diff d.md_syms kn in
let unk = Mid.set_diff d.pd_syms kn in
if Sid.is_empty unk then kn else
raise (Decl.UnknownIdent (Sid.choose unk))
src/mlw/mdecl.mli → src/mlw/pdecl.mli
View file @ e59abf8f
......@@ -41,44 +41,44 @@ val create_rec_variant_decl : itysymbol ->
(** {2 Module declarations} *)
type mdecl = private {
md_node : mdecl_node;
md_pure : Decl.decl list;
md_syms : Sid.t;
md_news : Sid.t;
md_tag : int;
type pdecl = private {
pd_node : pdecl_node;
pd_pure : Decl.decl list;
pd_syms : Sid.t;
pd_news : Sid.t;
pd_tag : int;
}
and mdecl_node = private
| MDtype of its_defn list
| MDlet of let_defn
| MDexn of xsymbol
| MDpure
and pdecl_node = private
| PDtype of its_defn list
| PDlet of let_defn
| PDexn of xsymbol
| PDpure
val create_type_decl : its_defn list -> mdecl
val create_type_decl : its_defn list -> pdecl
val create_let_decl : let_defn -> mdecl
val create_let_decl : let_defn -> pdecl
val create_exn_decl : xsymbol -> mdecl
val create_exn_decl : xsymbol -> pdecl
val create_pure_decl : Decl.decl -> mdecl
val create_pure_decl : Decl.decl -> pdecl
(** {2 Built-in decls} *)
val md_int : mdecl
val md_real : mdecl
val md_equ : mdecl
val md_bool : mdecl
val md_unit : mdecl
val md_tuple : int -> mdecl
val md_func : mdecl
val md_pred : mdecl
val md_func_app : mdecl
val pd_int : pdecl
val pd_real : pdecl
val pd_equ : pdecl
val pd_bool : pdecl
val pd_unit : pdecl
val pd_tuple : int -> pdecl
val pd_func : pdecl
val pd_pred : pdecl
val pd_func_app : pdecl
(** {2 Known identifiers} *)
type known_map = mdecl Mid.t
type known_map = pdecl Mid.t
val known_id : known_map -> ident -> unit
val known_add_decl : known_map -> mdecl -> known_map
val known_add_decl : known_map -> pdecl -> known_map
val merge_known : known_map -> known_map -> known_map
src/mlw/wmodule.ml → src/mlw/pmodule.ml
View file @ e59abf8f
......@@ -15,7 +15,7 @@ open Ty
open Theory
open Ity
open Expr
open Mdecl
open Pdecl
(** *)
......@@ -89,22 +89,22 @@ let ns_find_xs ns s = match ns_find_prog_symbol ns s with
(** {2 Module} *)
type wmodule = {
mod_theory : theory; (* pure theory *)
mod_decls : mdecl list; (* module declarations *)
mod_export : namespace; (* exported namespace *)
mod_known : known_map; (* known identifiers *)
mod_local : Sid.t; (* locally declared idents *)
mod_used : Sid.t; (* used modules *)
type pmodule = {
mod_theory : theory; (* pure theory *)
mod_decls : pdecl list; (* module declarations *)
mod_export : namespace; (* exported namespace *)
mod_known : known_map; (* known identifiers *)
mod_local : Sid.t; (* locally declared idents *)
mod_used : Sid.t; (* used modules *)
}
(** {2 Module under construction} *)
type wmodule_uc = {
type pmodule_uc = {
muc_theory : theory_uc;
muc_name : string;
muc_path : string list;
muc_decls : mdecl list;
muc_decls : pdecl list;
muc_prefix : string list;
muc_import : namespace list;
muc_export : namespace list;
......@@ -162,10 +162,10 @@ let close_namespace uc ~import =
let i1 = add_ns false s e0 i1 in
let e1 = add_ns true s e0 e1 in
{ uc with
muc_theory = th;
muc_theory = th;
muc_prefix = prf;
muc_import = i1 :: sti;
muc_export = e1 :: ste; }
muc_import = i1 :: sti;
muc_export = e1 :: ste; }
| _ ->
assert false
......@@ -219,17 +219,17 @@ let add_symbol add id v uc =
let add_meta uc m al =
{ uc with muc_theory = Theory.add_meta uc.muc_theory m al }
let add_mdecl ~wp uc d =
let add_pdecl ~wp uc d =
let uc = { uc with
muc_decls = d :: uc.muc_decls;
muc_known = known_add_decl uc.muc_known d;
muc_local = Sid.union uc.muc_local d.md_news } in
muc_local = Sid.union uc.muc_local d.pd_news } in
(* TODO
let uc = pdecl_ns uc d in
let uc = pdecl_vc ~wp uc d in
*)
ignore wp; (* TODO *)
let th = List.fold_left Theory.add_decl uc.muc_theory d.md_pure in
let th = List.fold_left Theory.add_decl uc.muc_theory d.pd_pure in
{ uc with muc_theory = th }
(** {2 Builtin symbols} *)
......@@ -239,11 +239,11 @@ let builtin_module =
let ns = add_ts true its_int.its_ts.ts_name.id_string its_int ns in
let ns = add_ts true its_real.its_ts.ts_name.id_string its_real ns in
let kn = Mid.empty in
let kn = known_add_decl kn md_int in
let kn = known_add_decl kn md_real in
let kn = known_add_decl kn md_equ in {
let kn = known_add_decl kn pd_int in
let kn = known_add_decl kn pd_real in
let kn = known_add_decl kn pd_equ in {
mod_theory = builtin_theory;
mod_decls = [md_int; md_real; md_equ];
mod_decls = [pd_int; pd_real; pd_equ];
mod_export = ns;
mod_known = kn;
mod_local = builtin_theory.th_local;
......@@ -251,16 +251,16 @@ let builtin_module =
let bool_module =
let uc = empty_module None (id_fresh "Bool") ["why3";"Bool"] in
let uc = add_mdecl ~wp:false uc md_bool in
let uc = add_pdecl ~wp:false uc pd_bool in
let md = close_module uc in
{ md with mod_theory = bool_theory }
let highord_module =
let uc = empty_module None (id_fresh "HighOrd") ["why3";"HighOrd"] in
let uc = use_export uc bool_module in
let uc = add_mdecl ~wp:false uc md_func in
let uc = add_mdecl ~wp:false uc md_pred in
let uc = add_mdecl ~wp:false uc md_func_app in
let uc = add_pdecl ~wp:false uc pd_func in
let uc = add_pdecl ~wp:false uc pd_pred in
let uc = add_pdecl ~wp:false uc pd_func_app in
let md = close_module uc in
{ md with mod_theory = highord_theory }
......@@ -272,12 +272,12 @@ let tuple_module_name s = Theory.tuple_theory_name s
let unit_module =
let uc = empty_module None (id_fresh "Unit") ["why3";"Unit"] in
let uc = use_export uc (tuple_module 0) in
let uc = add_mdecl ~wp:false uc md_unit in
let uc = add_pdecl ~wp:false uc pd_unit in
let md = close_module uc in
{ md with mod_theory = unit_theory }
*)
let add_mdecl_with_tuples _uc _md = assert false (*TODO*)
let add_pdecl_with_tuples _uc _md = assert false (*TODO*)
let create_module env ?(path=[]) n =
let m = empty_module (Some env) n path in
......@@ -291,12 +291,12 @@ let create_module env ?(path=[]) n =
(** {2 WhyML language} *)
type mlw_file = wmodule Mstr.t * theory Mstr.t
type mlw_file = pmodule Mstr.t * theory Mstr.t
let mlw_language =
(Env.register_language Env.base_language snd : mlw_file Env.language)
(* TODO
(* TODO
let () = Env.add_builtin mlw_language (function
| [s] when s = mod_prelude.mod_theory.th_name.id_string ->
Mstr.singleton s mod_prelude,
......
src/mlw/wmodule.mli → src/mlw/pmodule.mli
View file @ e59abf8f
......@@ -14,7 +14,7 @@ open Ident
open Theory
open Ity
open Expr
open Mdecl
open Pdecl
(** *)
......@@ -41,22 +41,22 @@ val ns_find_ns : namespace -> string list -> namespace
(** {2 Module} *)
type wmodule = private {
mod_theory : theory; (* pure theory *)
mod_decls : mdecl list; (* module declarations *)
mod_export : namespace; (* exported namespace *)
mod_known : known_map; (* known identifiers *)
mod_local : Sid.t; (* locally declared idents *)
mod_used : Sid.t; (* used modules *)
type pmodule = private {
mod_theory : theory; (* pure theory *)
mod_decls : pdecl list; (* module declarations *)
mod_export : namespace; (* exported namespace *)
mod_known : known_map; (* known identifiers *)
mod_local : Sid.t; (* locally declared idents *)
mod_used : Sid.t; (* used modules *)
}
(** {2 Module under construction} *)
type wmodule_uc = private {
type pmodule_uc = private {
muc_theory : theory_uc;
muc_name : string;
muc_path : string list;
muc_decls : mdecl list;
muc_decls : pdecl list;
muc_prefix : string list;
muc_import : namespace list;
muc_export : namespace list;
......@@ -66,11 +66,11 @@ type wmodule_uc = private {
muc_env : Env.env option;
}
val create_module : Env.env -> ?path:string list -> preid -> wmodule_uc
val close_module : wmodule_uc -> wmodule
val create_module : Env.env -> ?path:string list -> preid -> pmodule_uc
val close_module : pmodule_uc -> pmodule
val open_namespace : wmodule_uc -> string -> wmodule_uc
val close_namespace : wmodule_uc -> import:bool -> wmodule_uc
val open_namespace : pmodule_uc -> string -> pmodule_uc
val close_namespace : pmodule_uc -> import:bool -> pmodule_uc
val restore_path : ident -> string list * string * string list
(** [restore_path id] returns the triple (library path, module,
......@@ -80,50 +80,50 @@ val restore_path : ident -> string list * string * string list
If [id] is a module name, the third component is an empty list.
Raises Not_found if the ident was never declared in/as a module. *)
val restore_module : theory -> wmodule
val restore_module : theory -> pmodule
(** retrieves a module from its underlying theory
raises [Not_found] if no such module exists *)
(** {2 Use and clone} *)
val use_export : wmodule_uc -> wmodule -> wmodule_uc
val use_export : pmodule_uc -> pmodule -> pmodule_uc
(** {2 Logic decls} *)
val add_meta : wmodule_uc -> meta -> meta_arg list -> wmodule_uc
val add_meta : pmodule_uc -> meta -> meta_arg list -> pmodule_uc
(** {2 Program decls} *)
val add_mdecl : wp:bool -> wmodule_uc -> mdecl -> wmodule_uc
(** [add_mdecl ~wp m d] adds declaration [d] in module [m].
val add_pdecl : wp:bool -> pmodule_uc -> pdecl -> pmodule_uc
(** [add_pdecl ~wp m d] adds declaration [d] in module [m].
If [wp] is [true], VC is computed and added to [m]. *)
(** {2 Builtin symbols} *)
val builtin_module : wmodule
val builtin_module : pmodule
val bool_module : wmodule
val bool_module : pmodule
(* TODO
val unit_module : wmodule
val unit_module : pmodule
*)
val highord_module : wmodule
val highord_module : pmodule
val tuple_module : int -> wmodule
val tuple_module : int -> pmodule
val tuple_module_name : string -> int option
val add_mdecl_with_tuples : wmodule_uc -> mdecl -> wmodule_uc
val add_pdecl_with_tuples : pmodule_uc -> pdecl -> pmodule_uc
(** {2 WhyML language} *)
open Env
type mlw_file = wmodule Mstr.t * theory Mstr.t
type mlw_file = pmodule Mstr.t * theory Mstr.t
val mlw_language : mlw_file language
exception ModuleNotFound of pathname * string
val read_module : env -> pathname -> string -> wmodule
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