Commit 094ab658 authored by Andrei Paskevich's avatar Andrei Paskevich

several improvements, refactorings, and fixes

- prevent leak of idents by separating them into two types:
  - "preid" -- user-created and non-unique
  - "ident" -- unique, generated from "preid" by various
               smart constructors: create_tysymbol, etc

  This guarantees that two different symbols never share
  an ident.

- no need to hashcons tysymbols, fsymbols, and psymbols,
  as they are unique by construction

- make separate hashconsing smart constructors for decl

- export namespace as a private record (no reason to not to)

- some code rearrangement in hashconsing of decls

- fix namespace merging in close_namespace

- namespace name can be just a string, no need to use ident
parent e0d252af
......@@ -33,29 +33,40 @@ and origin =
module Id = struct
type t = ident
let equal = (==)
let hash id1 = id1.id_tag
let equal id1 id2 = id1.id_tag == id2.id_tag
let compare id1 id2 = Pervasives.compare id1.id_tag id2.id_tag
end
module Mid = Map.Make(Id)
module Sid = Set.Make(Id)
module Hid = Hashtbl.Make(Id)
type preid = ident
(* constructors *)
let gentag = let r = ref 0 in fun () -> incr r; !r
let id_register id = { id with id_tag = gentag () }
let create_ident short long origin = {
id_short = short;
id_long = long;
id_origin = origin;
id_tag = gentag ()
id_tag = -1
}
let id_fresh sh ln = create_ident sh ln Fresh
let id_derive sh ln id = create_ident sh ln (Derived id)
let id_fresh sh = create_ident sh sh Fresh
let id_fresh_long sh ln = create_ident sh ln Fresh
let id_user sh loc = create_ident sh sh (User loc)
let id_user_long sh ln loc = create_ident sh ln (User loc)
let id_derive sh id = create_ident sh sh (Derived id)
let id_derive_long sh ln id = create_ident sh ln (Derived id)
let id_clone id = create_ident id.id_short id.id_long (Derived id)
let id_user sh ln loc = create_ident sh ln (User loc)
let id_dup id = { id with id_tag = -1 }
(** Unique names for pretty printing *)
......@@ -77,7 +88,7 @@ let find_unique indices name =
name
let id_unique (indices,values) id =
try
try
Hashtbl.find values id.id_tag
with Not_found ->
let name = find_unique indices id.id_long in
......
......@@ -35,17 +35,29 @@ module Sid : Set.S with type elt = ident
module Mid : Map.S with type key = ident
module Hid : Hashtbl.S with type key = ident
(* create a fresh ident *)
val id_fresh : string -> string -> ident
(* a user-created type of unregistered identifiers *)
type preid
(* create a derived ident *)
val id_derive : string -> string -> ident -> ident
(* register a pre-ident (never use this function) *)
val id_register : preid -> ident
(* create a derived ident with the same name *)
val id_clone : ident -> ident
(* create a fresh pre-ident *)
val id_fresh : string -> preid
val id_fresh_long : string -> string -> preid
(* create a localized ident *)
val id_user : string -> string -> Loc.position -> ident
(* create a localized pre-ident *)
val id_user : string -> Loc.position -> preid
val id_user_long : string -> string -> Loc.position -> preid
(* create a derived pre-ident *)
val id_derive : string -> ident -> preid
val id_derive_long : string -> string -> ident -> preid
(* create a derived pre-ident with the same name *)
val id_clone : ident -> preid
(* create a duplicate pre-ident *)
val id_dup : ident -> preid
(** Unique persistent names for pretty printing *)
......
......@@ -21,7 +21,7 @@ type t = { tag : int ; name : string }
let fresh =
let cnt = ref 0 in
fun t ->
fun t ->
let tag = !cnt in
incr cnt;
{ t with tag = tag }
......@@ -38,8 +38,8 @@ let name_map = Hashtbl.create 47
let default_string = "anon"
let strip_numbers s =
let rec aux n =
let strip_numbers s =
let rec aux n =
if n <= 0 then 0
else
match s.[n-1] with
......@@ -48,7 +48,7 @@ let strip_numbers s =
let n = aux (String.length s) in
if n = 0 then default_string else String.sub s 0 n
let fresh_string name =
let fresh_string name =
let s = strip_numbers name in
try
let i = Hashtbl.find name_map s in
......@@ -74,10 +74,10 @@ module S = Set.Make (HT)
let get_cur_name, reset =
let current_name_map = H.create 47 in
let reset () =
H.clear current_name_map;
let reset () =
H.clear current_name_map;
Hashtbl.clear name_map in
let get_name x =
let get_name x =
try H.find current_name_map x
with Not_found ->
let s = to_string x in
......@@ -86,12 +86,12 @@ let get_cur_name, reset =
get_name, reset
let to_string = get_cur_name
let print fmt x = Format.fprintf fmt "%s" (get_cur_name x)
let build_map nl =
let m,_ =
List.fold_left (fun (m, i) n -> M.add n i m, i + 1)
let build_map nl =
let m,_ =
List.fold_left (fun (m, i) n -> M.add n i m, i + 1)
(M.empty, 0) nl in
m
......@@ -26,25 +26,26 @@ open Ty
type vsymbol = {
vs_name : ident;
vs_ty : ty;
vs_tag : int;
}
module Vsym = struct
type t = vsymbol
let equal vs1 vs2 = vs1.vs_name == vs2.vs_name
let equal = (==)
let hash vs = vs.vs_name.id_tag
let tag n vs = { vs with vs_tag = n }
let compare vs1 vs2 = Pervasives.compare vs1.vs_tag vs2.vs_tag
let compare vs1 vs2 =
Pervasives.compare vs1.vs_name.id_tag vs2.vs_name.id_tag
end
module Hvs = Hashcons.Make(Vsym)
module Mvs = Map.Make(Vsym)
module Svs = Set.Make(Vsym)
module Hvs = Hashtbl.Make(Vsym)
let mk_vs name ty = { vs_name = name; vs_ty = ty; vs_tag = -1 }
let create_vsymbol name ty = Hvs.hashcons (mk_vs name ty)
let create_vsymbol name ty = {
vs_name = id_register name;
vs_ty = ty;
}
let fresh_vsymbol v = create_vsymbol (id_clone v.vs_name) v.vs_ty
let fresh_vsymbol v = create_vsymbol (id_dup v.vs_name) v.vs_ty
(** Function symbols *)
......@@ -52,50 +53,47 @@ type fsymbol = {
fs_name : ident;
fs_scheme : ty list * ty;
fs_constr : bool;
fs_tag : int;
}
module Fsym = struct
type t = fsymbol
let equal fs1 fs2 = fs1.fs_name == fs2.fs_name
let equal = (==)
let hash fs = fs.fs_name.id_tag
let tag n fs = { fs with fs_tag = n }
let compare fs1 fs2 = Pervasives.compare fs1.fs_tag fs2.fs_tag
let compare fs1 fs2 =
Pervasives.compare fs1.fs_name.id_tag fs2.fs_name.id_tag
end
module Hfs = Hashcons.Make(Fsym)
module Sfs = Set.Make(Fsym)
module Mfs = Map.Make(Fsym)
module Hfs = Hashtbl.Make(Fsym)
let mk_fs name scheme constr = {
fs_name = name;
let create_fsymbol name scheme constr = {
fs_name = id_register name;
fs_scheme = scheme;
fs_constr = constr;
fs_tag = -1
}
let create_fsymbol name scheme constr = Hfs.hashcons (mk_fs name scheme constr)
(** Predicate symbols *)
type psymbol = {
ps_name : ident;
ps_scheme : ty list;
ps_tag : int;
}
module Psym = struct
type t = psymbol
let equal ps1 ps2 = ps1.ps_name == ps2.ps_name
let equal = (==)
let hash ps = ps.ps_name.id_tag
let tag n ps = { ps with ps_tag = n }
let compare ps1 ps2 = Pervasives.compare ps1.ps_tag ps2.ps_tag
let compare ps1 ps2 =
Pervasives.compare ps1.ps_name.id_tag ps2.ps_name.id_tag
end
module Hps = Hashcons.Make(Psym)
module Sps = Set.Make(Psym)
module Mps = Map.Make(Psym)
module Hps = Hashtbl.Make(Psym)
let mk_ps name scheme = { ps_name = name; ps_scheme = scheme; ps_tag = -1 }
let create_psymbol name scheme = Hps.hashcons (mk_ps name scheme)
let create_psymbol name scheme = {
ps_name = id_register name;
ps_scheme = scheme;
}
(** Patterns *)
......@@ -129,9 +127,9 @@ module Hpat = struct
let hash_node = function
| Pwild -> 0
| Pvar v -> v.vs_tag
| Papp (s, pl) -> Hashcons.combine_list hash_pattern s.fs_tag pl
| Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_tag
| Pvar v -> v.vs_name.id_tag
| Papp (s, pl) -> Hashcons.combine_list hash_pattern s.fs_name.id_tag pl
| Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_name.id_tag
let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
......@@ -289,16 +287,16 @@ module T = struct
let t_hash_branch (p, _, t) = Hashcons.combine p.pat_tag t.t_tag
let t_hash_bound (v, t) = Hashcons.combine v.vs_tag t.t_tag
let t_hash_bound (v, t) = Hashcons.combine v.vs_name.id_tag t.t_tag
let f_hash_bound (v, f) = Hashcons.combine v.vs_tag f.f_tag
let f_hash_bound (v, f) = Hashcons.combine v.vs_name.id_tag f.f_tag
let t_hash t = t.t_tag
let t_hash_node = function
| Tbvar n -> n
| Tvar v -> v.vs_tag
| Tapp (f, tl) -> Hashcons.combine_list t_hash (f.fs_tag) tl
| Tvar v -> v.vs_name.id_tag
| Tapp (f, tl) -> Hashcons.combine_list t_hash (f.fs_name.id_tag) tl
| Tlet (t, bt) -> Hashcons.combine t.t_tag (t_hash_bound bt)
| Tcase (t, bl) -> Hashcons.combine_list t_hash_branch t.t_tag bl
| Teps f -> f_hash_bound f
......@@ -354,14 +352,14 @@ module F = struct
let f_hash_branch (p, _, f) = Hashcons.combine p.pat_tag f.f_tag
let f_hash_bound (v, f) = Hashcons.combine v.vs_tag f.f_tag
let f_hash_bound (v, f) = Hashcons.combine v.vs_name.id_tag f.f_tag
let t_hash t = t.t_tag
let f_hash f = f.f_tag
let f_hash_node = function
| Fapp (p, tl) -> Hashcons.combine_list t_hash p.ps_tag tl
| Fapp (p, tl) -> Hashcons.combine_list t_hash p.ps_name.id_tag tl
| Fquant (q, bf) -> Hashcons.combine (Hashtbl.hash q) (f_hash_bound bf)
| Fbinop (op, f1, f2) ->
Hashcons.combine2 (Hashtbl.hash op) f1.f_tag f2.f_tag
......
......@@ -29,13 +29,13 @@ exception ConstructorExpected
type vsymbol = private {
vs_name : ident;
vs_ty : ty;
vs_tag : int;
}
module Svs : Set.S with type elt = vsymbol
module Mvs : Map.S with type key = vsymbol
module Hvs : Hashtbl.S with type key = vsymbol
val create_vsymbol : ident -> ty -> vsymbol
val create_vsymbol : preid -> ty -> vsymbol
(** Function symbols *)
......@@ -43,26 +43,26 @@ type fsymbol = private {
fs_name : ident;
fs_scheme : ty list * ty;
fs_constr : bool;
fs_tag : int;
}
val create_fsymbol : ident -> ty list * ty -> bool -> fsymbol
val create_fsymbol : preid -> ty list * ty -> bool -> fsymbol
module Sfs : Set.S with type elt = fsymbol
module Mfs : Map.S with type key = fsymbol
module Hfs : Hashtbl.S with type key = fsymbol
(** Predicate symbols *)
type psymbol = private {
ps_name : ident;
ps_scheme : ty list;
ps_tag : int;
}
val create_psymbol : ident -> ty list -> psymbol
val create_psymbol : preid -> ty list -> psymbol
module Sps : Set.S with type elt = psymbol
module Mps : Map.S with type key = psymbol
module Hps : Hashtbl.S with type key = psymbol
(** Patterns *)
......
......@@ -23,59 +23,155 @@ open Ident
open Ty
open Term
(** Error reporting *)
(** Declarations *)
exception CloseTheory
exception NoOpenedNamespace
exception RedeclaredIdent of ident
exception CannotInstantiate
exception ClashSymbol of string
(** The environment type *)
(* type declaration *)
module M = Map.Make(String)
type ty_def =
| Tabstract
| Talgebraic of fsymbol list
type ty_def =
| Ty_abstract
| Ty_algebraic of fsymbol list
type ty_decl = tysymbol * ty_def
type ty_decl = tysymbol * ty_def
(* logic declaration *)
type logic_decl =
type logic_decl =
| Lfunction of fsymbol * (vsymbol list * term) option (* FIXME: binders *)
| Lpredicate of psymbol * (vsymbol list * fmla) option (* FIXME: binders *)
| Linductive of psymbol * (ident * fmla) list
type prop_kind =
| Axiom | Lemma | Goal
(* proposition declaration *)
type prop_kind =
| Paxiom
| Plemma
| Pgoal
type prop_decl = prop_kind * ident * fmla
(* declaration *)
type decl_node =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_kind * ident * fmla
| Dprop of prop_decl
type decl = {d_node : decl_node; d_tag : int}
type decl = {
d_node : decl_node;
d_tag : int;
}
type decl_or_use =
| Decl of decl
| Use of theory
module D = struct
type t = decl
let for_all2 pr l1 l2 =
try List.for_all2 pr l1 l2 with Invalid_argument _ -> false
let eq_td (ts1,td1) (ts2,td2) = ts1 == ts2 && match td1,td2 with
| Tabstract, Tabstract -> true
| Talgebraic l1, Talgebraic l2 -> for_all2 (==) l1 l2
| _ -> false
let eq_fd fs1 fs2 fd1 fd2 = fs1 == fs2 && match fd1,fd2 with
| None, None -> true
| Some (l1,t1), Some (l2,t2) -> t1 == t2 && for_all2 (==) l1 l2
| _ -> false
let eq_ld ld1 ld2 = match ld1,ld2 with
| Lfunction (fs1,fd1), Lfunction (fs2,fd2) -> eq_fd fs1 fs2 fd1 fd2
| Lpredicate (ps1,pd1), Lpredicate (ps2,pd2) -> eq_fd ps1 ps2 pd1 pd2
| Linductive (ps1,l1), Linductive (ps2,l2) -> ps1 == ps2 &&
for_all2 (fun (i1,f1) (i2,f2) -> i1 == i2 && f1 == f2) l1 l2
| _ -> false
let equal d1 d2 = match d1.d_node, d2.d_node with
| Dtype l1, Dtype l2 -> for_all2 eq_td l1 l2
| Dlogic l1, Dlogic l2 -> for_all2 eq_ld l1 l2
| Dprop (k1,i1,f1), Dprop (k2,i2,f2) -> k1 == k2 && i1 == i2 && f1 == f2
| _ -> false
let hs_td (ts,td) = match td with
| Tabstract -> ts.ts_name.id_tag
| Talgebraic l ->
let tag fs = fs.fs_name.id_tag in
1 + Hashcons.combine_list tag ts.ts_name.id_tag l
let hs_ld ld = match ld with
| Lfunction (fs,fd) ->
let tag vs = vs.vs_name.id_tag in
let hsh (l,t) = Hashcons.combine_list tag t.t_tag l in
Hashcons.combine fs.fs_name.id_tag (Hashcons.combine_option hsh fd)
| Lpredicate (ps,pd) ->
let tag vs = vs.vs_name.id_tag in
let hsh (l,f) = Hashcons.combine_list tag f.f_tag l in
Hashcons.combine ps.ps_name.id_tag (Hashcons.combine_option hsh pd)
| Linductive (ps,l) ->
let hs_pair (i,f) = Hashcons.combine i.id_tag f.f_tag in
Hashcons.combine_list hs_pair ps.ps_name.id_tag l
let hash d = match d.d_node with
| Dtype l -> Hashcons.combine_list hs_td 0 l
| Dlogic l -> Hashcons.combine_list hs_ld 1 l
| Dprop (Paxiom,i,f) -> Hashcons.combine2 0 i.id_tag f.f_tag
| Dprop (Plemma,i,f) -> Hashcons.combine2 1 i.id_tag f.f_tag
| Dprop (Pgoal, i,f) -> Hashcons.combine2 2 i.id_tag f.f_tag
let tag n d = { d with d_tag = n }
let compare d1 d2 = Pervasives.compare d1.d_tag d2.d_tag
end
module Hdecl = Hashcons.Make(D)
module Mdecl = Map.Make(D)
module Sdecl = Set.Make(D)
and theory = {
th_name : ident;
th_param : Sid.t; (* locally declared abstract symbols *)
th_known : ident Mid.t; (* imported and locally declared symbols *)
th_export : namespace;
th_decls : decl_or_use list;
(* smart constructors *)
let mk_decl n = { d_node = n; d_tag = -1 }
let create_type tdl = Hdecl.hashcons (mk_decl (Dtype tdl))
let create_logic ldl = Hdecl.hashcons (mk_decl (Dlogic ldl))
let create_prop k i f = Hdecl.hashcons (mk_decl (Dprop (k, id_register i, f)))
(** Theory *)
module Snm = Set.Make(String)
module Mnm = Map.Make(String)
type theory = {
th_name : ident;
th_param : Sid.t; (* locally declared abstract symbols *)
th_known : ident Mid.t; (* imported and locally declared symbols *)
th_export : namespace;
th_decls : decl_or_use list;
}
and namespace = {
tysymbols : tysymbol M.t; (* type symbols *)
fsymbols : fsymbol M.t; (* function symbols *)
psymbols : psymbol M.t; (* predicate symbols *)
props : fmla M.t; (* formula *)
namespace : namespace M.t;
ns_ts : tysymbol Mnm.t; (* type symbols *)
ns_fs : fsymbol Mnm.t; (* function symbols *)
ns_ps : psymbol Mnm.t; (* predicate symbols *)
ns_ns : namespace Mnm.t; (* inner namespaces *)
ns_prop : fmla Mnm.t; (* propositions *)
}
and decl_or_use =
| Decl of decl
| Use of theory
(** Error reporting *)
exception CloseTheory
exception NoOpenedNamespace
exception RedeclaredIdent of ident
exception CannotInstantiate
exception ClashSymbol of string
(** Theory under construction *)
type theory_uc = {
uc_name : ident;
uc_param : Sid.t;
......@@ -86,181 +182,93 @@ type theory_uc = {
uc_decls : decl_or_use list;
}
(** Hashconsing of decl_node *)
module Hsh = Hashcons
module TDecl =
struct
type t = decl
let hash t =
match t.d_node with
| Dtype tyl ->
let htyd acc = function
| Ty_abstract -> acc
| Ty_algebraic fsl -> 1 +
Hsh.combine_list (fun x -> x.fs_tag) acc fsl in
let hty (tys,tyd) = htyd tys.ts_tag tyd in
Hsh.combine_list hty 0 tyl
| Dlogic ldl ->
let ldhash = function
| Lfunction (fs,opt) ->
let hvslt (vsl,t) = Hsh.combine_list (fun x -> x.vs_tag)
t.t_tag vsl in
Hsh.combine fs.fs_tag (Hsh.combine_option hvslt opt)
| Lpredicate (ps,opt) ->
let hvslt (vsl,f) = Hsh.combine_list (fun x -> x.vs_tag)
f.f_tag vsl in
Hsh.combine ps.ps_tag (Hsh.combine_option hvslt opt)
| Linductive (ps,ifl) ->
let hif (i,f) = Hsh.combine i.Ident.id_tag f.f_tag in
Hsh.combine_list hif ps.ps_tag ifl
in
Hsh.combine_list ldhash 0 ldl
| Dprop (k,i,f) ->
let hk = match k with
| Axiom -> 1
| Lemma -> 2
| Goal -> 3 in
Hsh.combine2 hk i.Ident.id_tag f.f_tag
let equal d1 d2 =
try
match d1.d_node,d2.d_node with
| Dtype tyl1, Dtype tyl2 -> List.for_all2
(fun (tys1,tyd1) (tys2,tyd2) -> tys1 == tys2 &&
match tyd1,tyd2 with
| Ty_abstract, Ty_abstract -> true
| Ty_algebraic fsl1, Ty_algebraic fsl2 ->
List.for_all2 (==) fsl1 fsl2
| _ -> false) tyl1 tyl2
| Dlogic ldl1, Dlogic ldl2 ->
let equal_funpred fs1 opt1 fs2 opt2 =
fs1 == fs2 &&
match opt1,opt2 with
| None, None -> true
| Some (vsl1,t1), Some (vsl2,t2) -> t1 == t2 &&
List.for_all2 (==) vsl1 vsl2
| _ -> false in
List.for_all2
(fun e1 e2 -> match e1,e2 with
| Lfunction (fs1, opt1),Lfunction (fs2, opt2) ->
equal_funpred fs1 opt1 fs2 opt2
| Lpredicate (ps1, opt1),Lpredicate (ps2, opt2) ->
equal_funpred ps1 opt1 ps2 opt2
| Linductive (ps1,ifl1), Linductive (ps2,ifl2) ->
ps1 == ps2 &&
List.for_all2 (fun (i1,f1) (i2,f2)-> i1 == i2 && f1 == f2)
ifl1 ifl2
| _ -> false) ldl1 ldl2
| Dprop (k1,i1,f1),Dprop (k2,i2,f2) -> i1 == i2 && f1 == f2 && k1 = k2
| _ -> false
with Invalid_argument _ -> false
let tag x t = {t with d_tag = x}
end
module Hdecl = Hashcons.Make(TDecl)
let hashdecl x = Hdecl.hashcons {d_node = x;d_tag = 0}
(** Creating environments *)
(* creating environments *)
let empty_ns = {
tysymbols = M.empty;
fsymbols = M.empty;
psymbols = M.empty;
props = M.empty;
namespace