Commit e0d252af authored by Francois Bobot's avatar Francois Bobot

Ajout du Hashconsing des decls

parent 6e8683d6
......@@ -51,7 +51,7 @@ OCAMLBEST= @OCAMLBEST@
OCAMLVERSION = @OCAMLVERSION@
CAMLP4 = @CAMLP4O@
INCLUDES = -I src/core -I src/util -I src/parser -I src
INCLUDES = -I src/core -I src/util -I src/parser -I src/transform -I src
BFLAGS = -w Aelz -dtypes -g $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
# no -warn-error because some do not compile all files (e.g. those linked to APRON)
OFLAGS = -w Aelz -dtypes $(INCLUDES) @INCLUDEGTK2@ -I +threads @OCAMLGRAPHLIB@
......@@ -106,7 +106,9 @@ UTIL_CMO = src/util/pp.cmo src/util/loc.cmo src/util/util.cmo \
src/util/hashcons.cmo
PARSER_CMO = src/parser/parser.cmo src/parser/lexer.cmo src/parser/typing.cmo
CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) src/pretty.cmo src/main.cmo
TRANSFORM_CMO = src/transform/transform.cmo
CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO) src/pretty.cmo src/main.cmo
CMX = $(CMO:.cmo=.cmx)
bin/why.opt: $(CMX)
......
......@@ -49,11 +49,13 @@ type logic_decl =
type prop_kind =
| Axiom | Lemma | Goal
type decl =
type decl_node =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_kind * ident * fmla
type decl = {d_node : decl_node; d_tag : int}
type decl_or_use =
| Decl of decl
| Use of theory
......@@ -84,6 +86,82 @@ 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 *)
let empty_ns = {
......@@ -265,7 +343,7 @@ let add_decl uc d =
let uc = add_known id uc in
add_symbol add_prop id f uc
in
{ uc with uc_decls = (Decl d) :: uc.uc_decls }
{ uc with uc_decls = (Decl (hashdecl d)) :: uc.uc_decls }
(** Querying environments *)
......
......@@ -35,11 +35,13 @@ type logic_decl =
type prop_kind =
| Axiom | Lemma | Goal
type decl =
type decl_node =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_kind * ident * fmla
type decl = private {d_node : decl_node; d_tag : int}
type decl_or_use =
| Decl of decl
| Use of theory
......@@ -74,7 +76,7 @@ type th_inst = {
val clone_export : theory_uc -> theory -> th_inst -> theory_uc
val add_decl : theory_uc -> decl -> theory_uc
val add_decl : theory_uc -> decl_node -> theory_uc
val close_theory : theory_uc -> theory
......
module type Sig =
sig
type t
val tag : t -> int
end
module type S =
sig
type elt
type t
val all : (elt list -> elt list) -> t
val fold_map_right : ('a -> elt -> ('a * elt list)) -> 'a -> t
val fold_map_left : ('a -> elt -> ('a * elt list)) -> 'a -> t
val elt : (elt -> elt list) -> t
val compose : t -> t -> t
val apply : t -> elt list -> elt list
val clear : t -> unit
end
module Make (X : Sig) =
struct
type elt = X.t
(* The datastructure for hashconsed list *)
module L =
struct
type t = (int * elt) list
let equal a b =
match a,b with
| [], [] -> true
| [], _ | _, [] -> false
(* work evenif al and bl are nil *)
| (_,ae)::al,(_,be)::bl -> X.tag ae = X.tag be && al == bl
let hash a =
match a with
| [] -> 0
| (_,ae)::[] -> X.tag ae
| (_,ae)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
let tag t = function
| [] -> []
| (_,ae)::al -> (t,ae)::al
end
module LH = Hashcons.Make(L)
let empty = []
let cons e l = LH.hashcons ((0,e)::l)
let tag_elt = X.tag
let tag_t = function
| [] -> -1
| (t,_)::_ -> t
(* the memoisation is inside the function *)
type t = { all : L.t -> L.t;
clear : unit -> unit;
memo_to_list : (int,elt list) Hashtbl.t }
let memo f tag h x =
try Hashtbl.find h (tag x:int)
with Not_found ->
let r = f x in
Hashtbl.add h (tag x) r;
r
let fold_map_left f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind edonev eltss =
let edone,_ = List.fold_left
(fun (edone,v) (tag,elts) ->
let v,l = f_fold v elts in
let edone = List.fold_left (fun e t -> cons t e) edone l in
Hashtbl.add memo_t tag (edone,v);
(edone,v)) edonev eltss in
edone in
let rec f acc t1 =
match t1 with
| [] -> rewind (empty,v_empty) acc
| (tag,e)::t2 ->
try
let edonev = Hashtbl.find memo_t tag in
rewind edonev acc
with Not_found -> f ((tag,e)::acc) t2
in
{all = f [];
clear = (fun () -> Hashtbl.clear memo_t);
memo_to_list = Hashtbl.create 16}
let elt f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt () x = (),memo f_elt tag_elt memo_elt x in
let f = fold_map_left f_elt () in
{f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
let fold_map_right f_fold v_empty =
let rec f (acc,v) t =
match t with
| [] -> List.fold_left (List.fold_left (fun t e -> cons e t)) empty acc
| (_,e)::t ->
let v,res = f_fold v e in
f (res::acc,v) t in
let memo_t = Hashtbl.create 16 in
{ all = memo (f ([],v_empty)) tag_t memo_t;
clear = (fun () -> Hashtbl.clear memo_t);
memo_to_list = Hashtbl.create 16}
let to_list =
let rec aux acc t =
match t with
| [] -> acc
| (_,e)::t -> aux (e::acc) t
in
aux []
let from_list = List.fold_left (fun t e -> cons e t) empty
let all f =
let f x = from_list (f (to_list x)) in
let memo_t = Hashtbl.create 16 in
{ all = memo f tag_t memo_t;
clear = (fun () -> Hashtbl.clear memo_t);
memo_to_list = Hashtbl.create 16}
let compose f g = {all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ());
memo_to_list = g.memo_to_list}
let apply f x =
let res = f.all (from_list x) in
memo to_list tag_t f.memo_to_list res
let clear f = f.clear ();Hashtbl.clear f.memo_to_list
end
open Term
open Ty
open Theory
module SDecl =
struct
type t = decl
let tag x = x.d_tag
end
module TDecl = Make(SDecl)
module SDecl_or_Use =
struct
type t = decl_or_use
let tag = function
| Decl d -> -d.d_tag
| Use t -> 1+t.th_name.Ident.id_tag
end
module TDecl_or_Use = Make(SDecl_or_Use)
(* Tranformation on list of element with some memoisations *)
(* The functors need a type with a tag function *)
module type Sig =
sig
type t
(* return an unique int for each element of t *)
val tag : t -> int
end
module type S =
sig
(* The type of the elements of the list*)
type elt
(* The type of the transformations on list of elt *)
type t
(* The general tranformation only one memoisation is performed with
the argument given *)
val all : (elt list -> elt list) -> t
(* map the element of the list from the first to the last.
only one memoisation is performed *)
val fold_map_right : ('a -> elt -> ('a * elt list)) -> 'a -> t
(* map the element of the list from the last to the first.
A memoisation is performed at each step *)
val fold_map_left : ('a -> elt -> ('a * elt list)) -> 'a -> t
(* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *)
val elt : (elt -> elt list) -> t
(* compose two transformation, the underliying datastructures for
the memoisation are shared *)
val compose : t -> t -> t
(* apply a transformation and memoise *)
val apply : t -> elt list -> elt list
(* clear the datastructures used to store the memoisation *)
val clear : t -> unit
end
module Make : functor (X : Sig) -> S with type elt = X.t
module TDecl : S with type elt = Theory.decl
module TDecl_or_Use : S with type elt = Theory.decl_or_use
......@@ -166,4 +166,7 @@ let combine acc n = n * 65599 + acc
let combine2 acc n1 n2 = combine acc (combine n1 n2)
let combine3 acc n1 n2 n3 = combine acc (combine n1 (combine n2 n3))
let combine_list f = List.fold_left (fun acc x -> combine acc (f x))
let combine_option h = function
| None -> 0
| Some s -> (h s) + 1
let combine_pair h1 h2 (a1,a2) = combine (h1 a1) (h2 a2)
......@@ -65,5 +65,5 @@ val combine : int -> int -> int
val combine2 : int -> int -> int -> int
val combine3 : int -> int -> int -> int -> int
val combine_list : ('a -> int) -> int -> 'a list -> int
val combine_option : ('a -> int) -> 'a option -> int
val combine_pair : ('a -> int) -> ('b -> int) -> 'a * 'b -> int
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