Commit 3be07314 authored by Andrei Paskevich's avatar Andrei Paskevich

bugfix: misuse of physical equality in Theory.ns_add

parent e0149985
......@@ -85,12 +85,14 @@ module Spr = Prop.S
module Mpr = Prop.M
module Hpr = Prop.H
let pr_equal = (==)
let pr_equal pr1 pr2 = id_equal pr1.pr_name pr2.pr_name
let create_prsymbol n = { pr_name = id_register n }
type prop = prsymbol * fmla
let prop_equal (pr1,f1) (pr2,f2) = pr_equal pr1 pr2 && f_equal f1 f2
type ind_decl = lsymbol * prop list
(** Proposition declaration *)
......
......@@ -63,6 +63,10 @@ type prop = prsymbol * fmla
type ind_decl = lsymbol * prop list
val pr_equal : prsymbol -> prsymbol -> bool
val prop_equal : prop -> prop -> bool
(* Proposition declaration *)
type prop_kind =
......
......@@ -45,26 +45,30 @@ let empty_ns = {
exception ClashSymbol of string
let ns_add chk x v m =
let ns_add eq chk x v m =
if not chk then Mnm.add x v m
else try
if Mnm.find x m != v then raise (ClashSymbol x);
if not (eq (Mnm.find x m) v) then raise (ClashSymbol x);
m
with Not_found -> Mnm.add x v m
let ts_add = ns_add ts_equal
let ls_add = ns_add ls_equal
let pr_add = ns_add prop_equal
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_pr = Mnm.fold (ns_add chk) ns1.ns_pr ns2.ns_pr;
{ ns_ts = Mnm.fold (ts_add chk) ns1.ns_ts ns2.ns_ts;
ns_ls = Mnm.fold (ls_add chk) ns1.ns_ls ns2.ns_ls;
ns_pr = Mnm.fold (pr_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_ts chk x ts ns = { ns with ns_ts = ts_add chk x ts ns.ns_ts }
let add_ls chk x ls ns = { ns with ns_ls = ls_add chk x ls ns.ns_ls }
let add_pr chk x pf ns = { ns with ns_pr = pr_add chk x pf ns.ns_pr }
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
......
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