program API: logic declarations in modules

parent 224229c4
......@@ -18,10 +18,43 @@
(**************************************************************************)
open Why3
open Util
open Ident
open Ty
open Decl
open Mlw_ty
type pdecl
type pdecl = {
pd_node : pdecl_node;
pd_syms : Sid.t; (* idents used in declaration *)
pd_news : Sid.t; (* idents introduced in declaration *)
pd_tag : int; (* unique tag *)
}
and pdecl_node
let pd_equal : pdecl -> pdecl -> bool = (==)
type known_map = pdecl Mid.t
let known_id kn id =
if not (Mid.mem id kn) then raise (UnknownIdent id)
let merge_known kn1 kn2 =
let check_known id decl1 decl2 =
if pd_equal decl1 decl2 then Some decl1
else raise (RedeclaredIdent id)
in
Mid.union check_known kn1 kn2
let known_add_decl kn0 decl =
let kn = Mid.map (const decl) decl.pd_news in
let check id decl0 _ =
if pd_equal decl0 decl
then raise (KnownIdent id)
else raise (RedeclaredIdent id)
in
let kn = Mid.union check kn0 kn in
let unk = Mid.set_diff decl.pd_syms kn in
if Sid.is_empty unk then kn
else raise (UnknownIdent (Sid.choose unk))
......@@ -22,6 +22,18 @@ open Ident
open Ty
open Mlw_ty
type pdecl
type pdecl = private {
pd_node : pdecl_node;
pd_syms : Sid.t; (* idents used in declaration *)
pd_news : Sid.t; (* idents introduced in declaration *)
pd_tag : int; (* unique tag *)
}
and pdecl_node
type known_map = pdecl Mid.t
val known_id : known_map -> ident -> unit
val known_add_decl : known_map -> pdecl -> known_map
val merge_known: known_map -> known_map -> known_map
......@@ -27,7 +27,7 @@ open Mlw_expr
open Mlw_decl
(*
module =
module =
theory +
namespace +
program decls (no logic decl here)
......@@ -98,6 +98,7 @@ type modul = {
mod_export: namespace; (* exported namespace *)
mod_known : known_map; (* known identifiers *)
mod_local : Sid.t; (* locally declared idents *)
mod_used : Sid.t; (* used modules *)
}
(** Module under construction *)
......@@ -109,6 +110,7 @@ type module_uc = {
muc_export : namespace list;
muc_known : known_map;
muc_local : Sid.t;
muc_used : Sid.t;
}
let empty_module n p = {
......@@ -118,6 +120,7 @@ let empty_module n p = {
muc_export = [empty_ns];
muc_known = Mid.empty;
muc_local = Sid.empty;
muc_used = Sid.empty;
}
let create_module ?(path=[]) n =
......@@ -129,7 +132,8 @@ let close_module uc =
mod_decls = List.rev uc.muc_decls;
mod_export = List.hd uc.muc_export;
mod_known = uc.muc_known;
mod_local = uc.muc_local; }
mod_local = uc.muc_local;
mod_used = uc.muc_used; }
let get_namespace uc = List.hd uc.muc_import
let get_known uc = uc.muc_known
......@@ -159,11 +163,45 @@ let close_namespace uc import s =
(** Use *)
(***
let use_export uc m =
let mth = m.mod_theory in
let id = mth.th_name in
let uc =
if not (Sid.mem id uc.muc_used) then
{ uc with
muc_known = merge_known uc.muc_known m.mod_known;
muc_used = Sid.add id uc.muc_used; }
else
uc
in
match uc.muc_import, uc.muc_export with
| i0 :: sti, e0 :: ste -> { uc with
muc_theory = Theory.use_export uc.muc_theory mth;
muc_import = merge_ns false m.mod_export i0 :: sti;
muc_export = merge_ns true m.mod_export e0 :: ste }
muc_export = merge_ns true m.mod_export e0 :: ste; }
| _ -> assert false
***)
(** Logic decls *)
let add_to_theory f uc x = { uc with muc_theory = f uc.muc_theory x }
let add_decl = add_to_theory Theory.add_decl
let add_decl_with_tuples = add_to_theory Theory.add_decl_with_tuples
let add_ty_decl = add_to_theory Theory.add_ty_decl
let add_logic_decl = add_to_theory Theory.add_logic_decl
let add_ind_decl = add_to_theory Theory.add_ind_decl
let add_prop_decl uc k pr f =
{ uc with muc_theory = Theory.add_prop_decl uc.muc_theory k pr f }
let use_export_theory = add_to_theory Theory.use_export
let clone_export_theory uc th i =
{ uc with muc_theory = Theory.clone_export uc.muc_theory th i }
let add_meta uc m al =
{ uc with muc_theory = Theory.add_meta uc.muc_theory m al }
(** Program decls *)
(*
val add_pdecl : module_uc -> pdecl -> module_uc
val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc
*)
......@@ -21,6 +21,8 @@ open Why3
open Util
open Ident
open Ty
open Term
open Decl
open Theory
open Mlw_ty
open Mlw_expr
......@@ -44,6 +46,7 @@ type modul = private {
mod_export: namespace; (* exported namespace *)
mod_known : known_map; (* known identifiers *)
mod_local : Sid.t; (* locally declared idents *)
mod_used : Sid.t; (* used modules *)
}
(** Module under construction *)
......@@ -61,6 +64,28 @@ val get_known : module_uc -> known_map
(** Use *)
(* val use_export : module_uc -> modul -> module_uc *)
val use_export : module_uc -> modul -> module_uc
(** Clone: not yet implemented *)
(** Clone *)
(* not yet implemented *)
(** Logic decls *)
val add_decl : module_uc -> decl -> module_uc
val add_decl_with_tuples : module_uc -> decl -> module_uc
val add_ty_decl : module_uc -> ty_decl list -> module_uc
val add_logic_decl : module_uc -> logic_decl list -> module_uc
val add_ind_decl : module_uc -> ind_decl list -> module_uc
val add_prop_decl : module_uc -> prop_kind -> prsymbol -> term -> module_uc
val use_export_theory: module_uc -> theory -> module_uc
val clone_export_theory: module_uc -> theory -> th_inst -> module_uc
val add_meta : module_uc -> meta -> meta_arg list -> module_uc
(** Program decls *)
(*
val add_pdecl : module_uc -> pdecl -> module_uc
val add_pdecl_with_tuples : module_uc -> pdecl -> module_uc
*)
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