Commit a4385564 authored by Andrei Paskevich's avatar Andrei Paskevich

clone instantiates namespaces (see examples/ns_clone.why)

parent 28913a16
theory Sig
type t
type elt
logic mem elt t
logic add elt t : t
axiom AddMem : forall e:elt, s:t. mem e (add e s)
end
theory Struct
type elt
type t = Empty | Holds elt
logic mem (e:elt) (s:t) = match s with
| Holds d -> e = d
| Empty -> false
end
logic add (e:elt) (s:t) : t = Holds e
(* this is the equivalent of Struct : Sig *)
clone Sig with namespace . = ., lemma AddMem
end
theory Shared
type obj = Roses | Violets
end
theory AbstractUser
use export Shared
clone import Sig with type elt = obj
logic program (s : t) : t = add Roses (add Violets s)
end
theory ConcreteUser
use export Shared
clone Struct as S with type elt = obj
(* note that the generated lemma AddMem is trivial,
since S contains an axiom of precisely the same form *)
clone export AbstractUser with namespace Sig = S, lemma Sig.AddMem
end
(*
AbstractUser acts as a functor on Sig. Or, to be more precise,
on Sig where type elt = Shared.obj. ConcreteUser instantiates
the implementation Struct on Shared.obj and then instantiates
AbstractUser on the resulting implementation S.
Note that the definition of the type obj cannot be given in
AbstractUser. Otherwise, we cannot define S in ConcreteUser.
In OCaml, can we constraint a functor's parameter with what
is defined in the functor itself?
Also note that "lemma AddMem" added to the clone statements
play the role of TCCs and/or refinement constraints. Later,
when we will start to clone program modules containing pre-
and post-conditions, these proof obligations would be produced
automatically.
*)
......@@ -39,8 +39,8 @@ type namespace = {
let empty_ns = {
ns_ts = Mnm.empty;
ns_ls = Mnm.empty;
ns_ns = Mnm.empty;
ns_pr = Mnm.empty;
ns_ns = Mnm.empty;
}
exception ClashSymbol of string
......@@ -79,6 +79,7 @@ let rec ns_find get_map ns = function
let ns_find_ts = ns_find (fun ns -> ns.ns_ts)
let ns_find_ls = ns_find (fun ns -> ns.ns_ls)
let ns_find_pr = ns_find (fun ns -> ns.ns_pr)
let ns_find_ns = ns_find (fun ns -> ns.ns_ns)
(** Meta properties *)
......
......@@ -37,6 +37,7 @@ type namespace = private {
val ns_find_ts : namespace -> string list -> tysymbol
val ns_find_ls : namespace -> string list -> lsymbol
val ns_find_pr : namespace -> string list -> prsymbol
val ns_find_ns : namespace -> string list -> namespace
(** Meta properties *)
......
......@@ -261,12 +261,18 @@ list1_comma_subst:
;
subst:
| NAMESPACE ns EQUAL ns { CSns ($2, $4) }
| TYPE qualid EQUAL qualid { CStsym ($2, $4) }
| LOGIC qualid EQUAL qualid { CSlsym ($2, $4) }
| LEMMA qualid { CSlemma $2 }
| GOAL qualid { CSgoal $2 }
;
ns:
| uqualid { Some $1 }
| DOT { None }
;
/* Meta args */
list1_meta_arg_sep_comma:
......
......@@ -97,6 +97,7 @@ type use = {
}
type clone_subst =
| CSns of qualid option * qualid option
| CStsym of qualid * qualid
| CSlsym of qualid * qualid
| CSlemma of qualid
......
......@@ -231,6 +231,9 @@ let find_tysymbol q uc = find_tysymbol_ns q (get_namespace uc)
let find_lsymbol_ns = find_ns ns_find_ls
let find_lsymbol q uc = find_lsymbol_ns q (get_namespace uc)
let find_namespace_ns = find_ns ns_find_ns
let find_namespace q uc = find_namespace_ns q (get_namespace uc)
let specialize_lsymbol p uc =
let s = find_lsymbol p uc in
let tl,ty = specialize_lsymbol ~loc:(qloc p) s in
......@@ -912,6 +915,29 @@ let find_theory env lenv q id = match q with
(* theory in file f *)
find_theory env q id
let rec clone_ns loc sl ns2 ns1 s =
let clash id = error ~loc (Clash id.id_string) in
let s = Mnm.fold (fun nm ns1 acc ->
if not (Mnm.mem nm ns2.ns_ns) then acc else
let ns2 = Mnm.find nm ns2.ns_ns in
clone_ns loc sl ns2 ns1 acc) ns1.ns_ns s
in
let inst_ts = Mnm.fold (fun nm ts1 acc ->
if not (Mnm.mem nm ns2.ns_ts) then acc else
if not (Sid.mem ts1.ts_name sl) then acc else
if Mts.mem ts1 acc then clash ts1.ts_name else
let ts2 = Mnm.find nm ns2.ns_ts in
Mts.add ts1 ts2 acc) ns1.ns_ts s.inst_ts
in
let inst_ls = Mnm.fold (fun nm ls1 acc ->
if not (Mnm.mem nm ns2.ns_ls) then acc else
if not (Sid.mem ls1.ls_name sl) then acc else
if Mls.mem ls1 acc then clash ls1.ls_name else
let ls2 = Mnm.find nm ns2.ns_ls in
Mls.add ls1 ls2 acc) ns1.ns_ls s.inst_ls
in
{ s with inst_ts = inst_ts; inst_ls = inst_ls }
let add_decl env lenv th = function
| TypeDecl dl ->
add_types dl th
......@@ -934,6 +960,11 @@ let add_decl env lenv th = function
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
......
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