Commit b8a9808d authored by Andrei Paskevich's avatar Andrei Paskevich

several modifications around namespaces:

- do not add to the new namespace the old instantiated names
- namespaces with the same name are merged instead of raising
  an exception.

Attention: examples clash_namespace1.why, already_theory1.why,
already_theory2.why, clash_type6.why, clash_type7.why migrated 
from bench/typing/bad/ to bench/typing/good/. Please, consult
these files and make sure you comprehend and approve the new
semantics.
parent ec14b110
......@@ -52,16 +52,20 @@ let ns_add chk x v m =
m
with Not_found -> Mnm.add x v m
let merge_ns chk ns1 ns2 =
let rec merge_ns chk ns1 ns2 =
{ ns_ts = Mnm.fold (ns_add chk) ns1.ns_ts ns2.ns_ts;
ns_ls = Mnm.fold (ns_add chk) ns1.ns_ls ns2.ns_ls;
ns_ns = Mnm.fold (ns_add chk) ns1.ns_ns ns2.ns_ns;
ns_pr = Mnm.fold (ns_add chk) ns1.ns_pr ns2.ns_pr; }
ns_pr = Mnm.fold (ns_add chk) ns1.ns_pr ns2.ns_pr;
ns_ns = Mnm.fold (fusion chk) ns1.ns_ns ns2.ns_ns; }
and fusion chk x ns m =
let os = try Mnm.find x m with Not_found -> empty_ns in
Mnm.add x (merge_ns chk os ns) m
let add_ts chk x ts ns = { ns with ns_ts = ns_add chk x ts ns.ns_ts }
let add_ls chk x ls ns = { ns with ns_ls = ns_add chk x ls ns.ns_ls }
let add_pr chk x pf ns = { ns with ns_pr = ns_add chk x pf ns.ns_pr }
let add_ns chk x nn ns = { ns with ns_ns = ns_add chk x nn ns.ns_ns }
let add_ns chk x nn ns = { ns with ns_ns = fusion chk x nn ns.ns_ns }
let rec ns_find get_map ns = function
| [] -> assert false
......@@ -481,22 +485,29 @@ let clone_export uc th inst =
let lc = Hid.fold add_local cl.nw_local uc.uc_local in
let uc = { uc with uc_local = lc } in
let find_ts ts =
if Sid.mem ts.ts_name th.th_local
then Hts.find cl.ts_table ts else ts in
let find_ls ls =
if Sid.mem ls.ls_name th.th_local
then Hls.find cl.ls_table ls else ls in
let find_pr (pr,f) =
if Sid.mem pr.pr_name th.th_local
then Hpr.find cl.pr_table pr else (pr,f) in
let f_ts n ts ns =
if Sid.mem ts.ts_name th.th_local then
let ts' = Hts.find cl.ts_table ts in
if Hid.mem cl.nw_local ts'.ts_name
then add_ts true n ts' ns else ns
else add_ts true n ts ns in
let f_ls n ls ns =
if Sid.mem ls.ls_name th.th_local then
let ls' = Hls.find cl.ls_table ls in
if Hid.mem cl.nw_local ls'.ls_name
then add_ls true n ls' ns else ns
else add_ls true n ls ns in
let f_pr n (pr,f) ns =
if Sid.mem pr.pr_name th.th_local then
if Hpr.mem cl.pr_table pr then
let (pr',f') = Hpr.find cl.pr_table pr in
if Hid.mem cl.nw_local pr'.pr_name
then add_pr true n (pr',f') ns else ns
else ns
else add_pr true n (pr,f) ns in
let f_ts n ts ns = add_ts true n (find_ts ts) ns in
let f_ls n ls ns = add_ls true n (find_ls ls) ns in
let f_pr n pr ns = try add_pr true n (find_pr pr) ns
with Not_found -> ns (* goals are not cloned *) in
let rec f_ns n s = add_ns true n (merge_namespace empty_ns s)
and merge_namespace acc ns =
......
......@@ -33,7 +33,6 @@ open Denv
type error =
| Message of string
| ClashType of string
| DuplicateTypeVar of string
| TypeArity of qualid * int * int
| Clash of string
......@@ -41,7 +40,6 @@ type error =
| TermExpected
| BadNumberOfArguments of Ident.ident * int * int
| ClashTheory of string
| ClashNamespace of string
| UnboundTheory of qualid
| AlreadyTheory of string
| UnboundFile of string
......@@ -77,8 +75,6 @@ let rec print_qualid fmt = function
let report fmt = function
| Message s ->
fprintf fmt "%s" s
| ClashType s ->
fprintf fmt "clash with previous type %s" s
| DuplicateTypeVar s ->
fprintf fmt "duplicate type parameter %s" s
| TypeArity (id, a, n) ->
......@@ -95,8 +91,6 @@ let report fmt = function
fprintf fmt "but is expecting %d arguments@]" m
| ClashTheory s ->
fprintf fmt "clash with previous theory %s" s
| ClashNamespace s ->
fprintf fmt "clash with previous namespace %s" s
| UnboundTheory q ->
fprintf fmt "unbound theory %a" print_qualid q
| AlreadyTheory s ->
......@@ -613,15 +607,8 @@ and fmla env = function
open Ptree
let add_types dl th =
let ns = get_namespace th in
let def =
List.fold_left
(fun def d ->
let id = d.td_ident in
if Mstr.mem id.id def || Mnm.mem id.id ns.ns_ts then
error ~loc:id.id_loc (ClashType id.id);
Mstr.add id.id d def)
Mstr.empty dl
List.fold_left (fun def d -> Mstr.add d.td_ident.id d def) Mstr.empty dl
in
let tysymbols = Hashtbl.create 17 in
let rec visit x =
......@@ -714,21 +701,18 @@ let env_of_vsymbol_list vl =
List.fold_left (fun env v -> Mstr.add v.vs_name.id_short v env) Mstr.empty vl
let add_logics dl th =
let ns = get_namespace th in
let fsymbols = Hashtbl.create 17 in
let psymbols = Hashtbl.create 17 in
let denvs = Hashtbl.create 17 in
(* 1. create all symbols and make an environment with these symbols *)
let create_symbol th d =
let id = d.ld_ident.id in
if Hashtbl.mem denvs id || Mnm.mem id ns.ns_ls
then error ~loc:d.ld_loc (Clash id);
let v = id_user id d.ld_loc in
let denv = create_denv th in
Hashtbl.add denvs id denv;
let type_ty (_,t) = ty_of_dty (dty denv t) in
let pl = List.map type_ty d.ld_params in
match d.ld_type with
try match d.ld_type with
| None -> (* predicate *)
let ps = create_psymbol v pl in
Hashtbl.add psymbols id ps;
......@@ -738,6 +722,7 @@ let add_logics dl th =
let fs = create_fsymbol v pl t in
Hashtbl.add fsymbols id fs;
add_decl th (create_logic_decl [fs, None])
with ClashSymbol s -> error ~loc:d.ld_loc (Clash s)
in
let th' = List.fold_left create_symbol th dl in
(* 2. then type-check all definitions *)
......@@ -807,28 +792,37 @@ let add_prop k loc s f th =
let f = fmla th f in
try
add_decl th (create_prop_decl k (create_prsymbol (id_user s.id loc)) f)
with ClashSymbol _ ->
error ~loc (Clash s.id)
with ClashSymbol s -> error ~loc (Clash s)
let loc_of_id id = match id.id_origin with
| User loc -> loc
| _ -> assert false
let add_inductives dl th =
let ns = get_namespace th in
let psymbols = Hashtbl.create 17 in
(* 0. create all propositional symbols *)
let propsyms = Hashtbl.create 17 in
let create_prsyms th (loc, id, _) =
let ps = create_prsymbol (id_user id.id loc) in
Hashtbl.add propsyms id.id ps;
try add_decl th (create_prop_decl Paxiom ps f_true)
with ClashSymbol s -> error ~loc (Clash s)
in
let create_prsyms th d =
List.fold_left create_prsyms th d.in_def
in
ignore (List.fold_left create_prsyms th dl);
(* 1. create all symbols and make an environment with these symbols *)
let psymbols = Hashtbl.create 17 in
let create_symbol th d =
let id = d.in_ident.id in
if Hashtbl.mem psymbols id || Mnm.mem id ns.ns_ls
then error ~loc:d.in_loc (Clash id);
let v = id_user id d.in_loc in
let denv = create_denv th in
let type_ty t = ty_of_dty (dty denv t) in
let pl = List.map type_ty d.in_params in
let ps = create_psymbol v pl in
Hashtbl.add psymbols id ps;
add_decl th (create_logic_decl [ps, None])
try add_decl th (create_logic_decl [ps, None])
with ClashSymbol s -> error ~loc:d.in_loc (Clash s)
in
let th' = List.fold_left create_symbol th dl in
(* 2. then type-check all definitions *)
......@@ -836,7 +830,7 @@ let add_inductives dl th =
let id = d.in_ident.id in
let ps = Hashtbl.find psymbols id in
let clause (loc, id, f) =
create_prsymbol (id_user id.id loc), fmla th' f
Hashtbl.find propsyms id.id, fmla th' f
in
ps, List.map clause d.in_def
in
......@@ -953,21 +947,14 @@ and add_decl env lenv th = function
close_namespace th true n
| Export ->
use_or_clone th
with ClashSymbol s ->
error ~loc (Clash s)
with ClashSymbol s -> error ~loc (Clash s)
end
| Namespace (_, import, name, dl) ->
let ns = get_namespace th in
let id = match name with
| Some { id=id; id_loc=loc } ->
if Mnm.mem id ns.ns_ns then error ~loc (ClashNamespace id);
Some id
| None ->
None
in
| Namespace (loc, import, name, dl) ->
let th = open_namespace th in
let th = add_decls env lenv th dl in
close_namespace th import id
let id = option_map (fun id -> id.id) name in
try close_namespace th import id
with ClashSymbol s -> error ~loc (Clash s)
and type_and_add_theory env lenv pt =
let id = pt.pt_name 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