Commit e5559996 authored by Francois Bobot's avatar Francois Bobot

ajout d'une premiere transformation non testee

parent d4d531d4
...@@ -106,7 +106,7 @@ UTIL_CMO = src/util/pp.cmo src/util/loc.cmo src/util/util.cmo \ ...@@ -106,7 +106,7 @@ UTIL_CMO = src/util/pp.cmo src/util/loc.cmo src/util/util.cmo \
src/util/hashcons.cmo src/util/hashcons.cmo
PARSER_CMO = src/parser/parser.cmo src/parser/lexer.cmo src/parser/typing.cmo PARSER_CMO = src/parser/parser.cmo src/parser/lexer.cmo src/parser/typing.cmo
TRANSFORM_CMO = src/transform/transform.cmo TRANSFORM_CMO = src/transform/transform.cmo src/transform/simplify_recursive_definition.cmo
CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO) src/pretty.cmo src/main.cmo CMO = $(UTIL_CMO) $(CORE_CMO) $(PARSER_CMO) $(TRANSFORM_CMO) src/pretty.cmo src/main.cmo
CMX = $(CMO:.cmo=.cmx) CMX = $(CMO:.cmo=.cmx)
......
...@@ -47,9 +47,37 @@ let rec print_term fmt t = match t.t_node with ...@@ -47,9 +47,37 @@ let rec print_term fmt t = match t.t_node with
fprintf fmt "(%a(%a) : %a)" fprintf fmt "(%a(%a) : %a)"
print_ident s.fs_name (print_list comma print_term) tl print_ident s.fs_name (print_list comma print_term) tl
print_ty t.t_ty print_ty t.t_ty
| _ -> | Tlet (t1,tbound) ->
assert false (*TODO*) let vs,t2 = t_open_bound tbound in
fprintf fmt "(let %a = %a in %a)"
print_ident vs.vs_name print_term t1 print_term t2
| Tcase _ -> assert false (*TODO*)
| Teps _ -> assert false
let rec print_fmla fmt f = let rec print_fmla fmt f = match f.f_node with
assert false (*TODO*) | Fapp (s,tl) ->
fprintf fmt "(%a(%a))"
print_ident s.ps_name (print_list comma print_term) tl
| Fquant (q,fbound) ->
let vs,f = f_open_bound fbound in
fprintf fmt "(%s %a : %a. %a)"
(match q with Fforall -> "forall" | Fexists -> "exists")
print_ident vs.vs_name print_ty vs.vs_ty print_fmla f
| Ftrue -> fprintf fmt "(true)"
| Ffalse -> fprintf fmt "(false)"
| Fbinop (b,f1,f2) ->
fprintf fmt "(%a %s %a)"
print_fmla f1
(match b with
| Fand -> "and" | For -> "or"
| Fimplies -> "->" | Fiff -> "<->")
print_fmla f2
| Fnot f -> fprintf fmt "(not %a)" print_fmla f
| _ -> assert false (*TODO*)
(*
let print_decl fmt d = match d.d_node with
| Dtype tl ->
| Dlogic ldl ->
| Dprop (k,id,fmla) ->
*)
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Ident
open Ty
open Term
open Theory
type seen =
| SNot
| SOnce
| SBack
let rec find h e =
try
let r = Hid.find h e in
if r == e then e
else
let r = find h r in
Hid.replace h e r;
r
with Not_found -> e
let union h e1 e2 = Hid.replace h (find h e1) (find h e2)
let connexe (m:Sid.t Mid.t) =
let uf = Hid.create 32 in
let visited = Hid.create 32 in
Mid.iter (fun e _ -> Hid.replace visited e SNot) m;
let rec visit i last =
match Hid.find visited i with
| SNot ->
Hid.replace visited i SOnce;
let s = Mid.find i m in
let last = i::last in
Sid.iter (fun x -> visit x last) s;
Hid.replace visited i SBack
| SOnce ->
(try
List.iter (fun e -> if e==i then raise Exit else union uf i e) last
with Exit -> ())
| SBack -> ()
in
Mid.iter (fun e _ -> visit e []) m;
let ce = Hid.create 32 in
Mid.iter (fun e es ->
let r = find uf e in
let rl,rs,rb = try
Hid.find ce r
with Not_found -> [],Sid.empty, ref false in
Hid.replace ce r (e::rl,Sid.union rs es,rb)) m;
let rec visit (l,s,b) acc =
if !b then acc
else
begin
b := true;
let acc = Sid.fold (fun e acc ->
try
visit (Hid.find ce e) acc
with Not_found -> acc) s acc in
l::acc
end
in
Hid.fold (fun _ -> visit) ce []
let elt d =
match d.d_node with
| Dprop _ -> [d]
| Dlogic l ->
let mem = Hid.create 16 in
List.iter (function
| Lfunction (fs,_) as a -> Hid.add mem fs.fs_name a
| Lpredicate (ps,_) as a -> Hid.add mem ps.ps_name a
| Linductive (ps,_) as a -> Hid.add mem ps.ps_name a) l;
let toccurences acc t =
match t.t_node with
| Tapp (fs,_) when Hid.mem mem fs.fs_name ->
Sid.add fs.fs_name acc
| _ -> acc in
let foccurences acc f =
match f.f_node with
| Fapp (ps,_) when Hid.mem mem ps.ps_name ->
Sid.add ps.ps_name acc
| _ -> acc in
let m = List.fold_left
(fun acc a -> match a with
| Lfunction (fs,l) ->
let s = match l with
| None -> Sid.empty
| Some (_,t) ->
t_fold_trans toccurences foccurences Sid.empty t in
Mid.add fs.fs_name s acc
| Lpredicate (ps,l) ->
let s = match l with
| None -> Sid.empty
| Some (_,f) ->
f_fold_trans toccurences foccurences Sid.empty f in
Mid.add ps.ps_name s acc
| Linductive (ps,l) ->
let s = List.fold_left
(fun acc (_,f) -> f_fold_trans toccurences foccurences acc f)
Sid.empty l in
Mid.add ps.ps_name s acc) Mid.empty l in
let l = connexe m in
List.map (fun e -> create_logic (List.map (Hid.find mem) e)) l
| Dtype l ->
let mem = Hid.create 16 in
List.iter (fun ((ts,_) as a) -> Hid.add mem ts.ts_name a) l;
let tyoccurences acc t =
match t.ty_node with
| Tyapp (ts,_) when Hid.mem mem ts.ts_name ->
Sid.add ts.ts_name acc
| _ -> acc in
let m = List.fold_left
(fun acc (ts,def) ->
let s = match def with
| Tabstract ->
begin match ts.ts_def with
| None -> Sid.empty
| Some ty -> ty_fold tyoccurences Sid.empty ty
end
| Talgebraic l ->
List.fold_left
(fun acc {fs_scheme = tyl,ty} ->
List.fold_left
(fun acc ty-> ty_fold tyoccurences acc ty) acc (ty::tyl)
) Sid.empty l in
Mid.add ts.ts_name s acc) Mid.empty l in
let l = connexe m in
List.map (fun e -> create_type (List.map (Hid.find mem) e)) l
let t = Transform.TDecl.elt elt
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* Simplify the recursive type and logic definition *)
val t : (Theory.decl,Theory.decl) Transform.t
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* This module has the invariant that each type has only one tag function *)
type 'a hashconsedlist = (int * 'a) list
module type Sig = module type Sig =
sig sig
type t type t
val tag : t -> int val tag : t -> int
end end
module type S = (* The datastructure for hashconsed list *)
sig module LH (X: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 struct
type elt = X.t module L =
(* The datastructure for hashconsed list *)
module L =
struct struct
type t = (int * elt) list type t = X.t hashconsedlist
let equal a b = let equal a b =
match a,b with match a,b with
| [], [] -> true | [], [] -> true
...@@ -39,31 +46,89 @@ struct ...@@ -39,31 +46,89 @@ struct
| (_,ae)::[] -> X.tag ae | (_,ae)::[] -> X.tag ae
| (_,ae)::(at,_)::_ -> Hashcons.combine (X.tag ae) at | (_,ae)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
let tag t = function let tag t = function
| [] -> [] | [] -> []
| (_,ae)::al -> (t,ae)::al | (_,ae)::al -> (t,ae)::al
end end
module LH = Hashcons.Make(L) module LH = Hashcons.Make(L)
type t = L.t
let empty : t = []
let cons e l : t = LH.hashcons ((0,e)::l)
let empty = [] let to_list : t -> X.t list =
let cons e l = LH.hashcons ((0,e)::l) let rec aux acc t =
let tag_elt = X.tag match t with
let tag_t = function | [] -> acc
| (_,e)::t -> aux (e::acc) t
in
aux []
let from_list = List.fold_left (fun t e -> cons e t) empty
let tag = function
| [] -> -1 | [] -> -1
| (t,_)::_ -> t | (t,_)::_ -> t
end
(* the memoisation is inside the function *)
type ('a,'b) t = { all : 'a hashconsedlist -> 'b hashconsedlist;
clear : unit -> unit;
from_list : 'a list -> 'a hashconsedlist;
to_list : 'b hashconsedlist -> 'b list;
clear_to_list : unit -> unit}
let compose f g = {all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ());
from_list = f.from_list;
to_list = g.to_list;
clear_to_list = g.clear_to_list}
let apply f x = f.to_list (f.all (f.from_list x))
let clear f = f.clear ();f.clear_to_list ()
(* the memoisation is inside the function *) let memo f tag h x =
type t = { all : L.t -> L.t; try Hashtbl.find h (tag x:int)
clear : unit -> unit; with Not_found ->
memo_to_list : (int,elt list) Hashtbl.t } let r = f x in
Hashtbl.add h (tag x) r;
r
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
module type S =
sig
type elt1
type elt2
val all : (elt1 list -> elt2 list) -> (elt1,elt2) t
val fold_map_right : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
val fold_map_left : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
val elt : (elt1 -> elt2 list) -> (elt1,elt2) t
end
module Make (X1 : Sig) (X2 : Sig) =
struct
type elt1 = X1.t
type elt2 = X2.t
module LH1 = LH(X1)
module LH2 = LH(X2)
let memo_to_list2 h : X2.t hashconsedlist -> X2.t list =
memo LH2.to_list LH2.tag h
let t all clear =
let h_to_list = Hashtbl.create 16 in
{all = all;
clear = clear;
from_list = LH1.from_list;
to_list = memo_to_list2 h_to_list;
clear_to_list = (fun () -> Hashtbl.clear h_to_list)
}
let fold_map_left f_fold v_empty = let fold_map_left f_fold v_empty =
let memo_t = Hashtbl.create 64 in let memo_t = Hashtbl.create 64 in
...@@ -71,68 +136,41 @@ struct ...@@ -71,68 +136,41 @@ struct
let edone,_ = List.fold_left let edone,_ = List.fold_left
(fun (edone,v) (tag,elts) -> (fun (edone,v) (tag,elts) ->
let v,l = f_fold v elts in let v,l = f_fold v elts in
let edone = List.fold_left (fun e t -> cons t e) edone l in let edone = List.fold_left (fun e t -> LH2.cons t e) edone l in
Hashtbl.add memo_t tag (edone,v); Hashtbl.add memo_t tag (edone,v);
(edone,v)) edonev eltss in (edone,v)) edonev eltss in
edone in edone in
let rec f acc t1 = let rec f acc t1 =
match t1 with match t1 with
| [] -> rewind (empty,v_empty) acc | [] -> rewind (LH2.empty,v_empty) acc
| (tag,e)::t2 -> | (tag,e)::t2 ->
try try
let edonev = Hashtbl.find memo_t tag in let edonev = Hashtbl.find memo_t tag in
rewind edonev acc rewind edonev acc
with Not_found -> f ((tag,e)::acc) t2 with Not_found -> f ((tag,e)::acc) t2
in in
{all = f []; t (f []) (fun () -> Hashtbl.clear memo_t)
clear = (fun () -> Hashtbl.clear memo_t);
memo_to_list = Hashtbl.create 16}
let elt f_elt = let elt f_elt =
let memo_elt = Hashtbl.create 64 in let memo_elt = Hashtbl.create 64 in
let f_elt () x = (),memo f_elt tag_elt memo_elt x in let f_elt () x = (),memo f_elt X1.tag memo_elt x in
let f = fold_map_left f_elt () in let f = fold_map_left f_elt () in
{f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()} {f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
let fold_map_right f_fold v_empty = let fold_map_right f_fold v_empty =
let rec f (acc,v) t = let rec f (acc,v) t =
match t with match t with
| [] -> List.fold_left (List.fold_left (fun t e -> cons e t)) empty acc | [] -> List.fold_left (List.fold_left (fun t e -> LH2.cons e t)) LH2.empty acc
| (_,e)::t -> | (_,e)::t ->
let v,res = f_fold v e in let v,res = f_fold v e in
f (res::acc,v) t in f (res::acc,v) t in
let memo_t = Hashtbl.create 16 in let memo_t = Hashtbl.create 16 in
{ all = memo (f ([],v_empty)) tag_t memo_t; t (memo (f ([],v_empty)) LH1.tag memo_t) (fun () -> Hashtbl.clear 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 all f =
let f x = from_list (f (to_list x)) in let f x = LH2.from_list (f (LH1.to_list x)) in
let memo_t = Hashtbl.create 16 in let memo_t = Hashtbl.create 16 in
{ all = memo f tag_t memo_t; t (memo f LH1.tag memo_t) (fun () -> Hashtbl.clear 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 end
open Term open Term
...@@ -145,7 +183,7 @@ module SDecl = ...@@ -145,7 +183,7 @@ module SDecl =
let tag x = x.d_tag let tag x = x.d_tag
end end
module TDecl = Make(SDecl) module TDecl = Make(SDecl)(SDecl)
module SDecl_or_Use = module SDecl_or_Use =
struct struct
...@@ -155,4 +193,14 @@ module SDecl_or_Use = ...@@ -155,4 +193,14 @@ module SDecl_or_Use =
| Use t -> 1+t.th_name.Ident.id_tag | Use t -> 1+t.th_name.Ident.id_tag
end end
module TDecl_or_Use = Make(SDecl_or_Use) module TDecl_or_Use = Make(SDecl_or_Use)(SDecl_or_Use)
module STheory =
struct
type t = theory
let tag t = t.th_name.Ident.id_tag
end
module TTheory = Make(STheory)(STheory)
module TTheory_Decl = Make(STheory)(SDecl)
(**************************************************************************)
(* *)
(* Copyright (C) 2010- *)
(* Francois Bobot *)
(* Jean-Christophe Filliatre *)
(* Johannes Kanig *)
(* Andrei Paskevich *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
(* Tranformation on list of element with some memoisations *) (* Tranformation on list of element with some memoisations *)
(* The functors need a type with a tag function *) (* The type of transformation from list of 'a to list of 'b *)
module type Sig = type ('a,'b) t
sig
type t (* compose two transformation, the underlying datastructures for
the memoisation are shared *)
val compose : ('a,'b) t -> ('b,'c) t -> ('a,'c) t
(* apply a transformation and memoise *)
val apply : ('a,'b) t -> 'a list -> 'b list
(* clear the datastructures used to store the memoisation *)
val clear : ('a,'b) t -> unit
(* return an unique int for each element of t *)
val tag : t -> int
end
module type S = module type S =
sig sig
(* The type of the elements of the list*) (* The type of the elements of the list*)
type elt type elt1
type elt2
(* The type of the transformations on list of elt *)
type t
(* The general tranformation only one memoisation is performed with (* The general tranformation only one memoisation is performed with
the argument given *) the argument given *)
val all : (elt list -> elt list) -> t val all : (elt1 list -> elt2 list) -> (elt1,elt2) t
(* map the element of the list from the first to the last. (* map the element of the list from the first to the last.
only one memoisation is performed *) only one memoisation is performed *)
val fold_map_right : ('a -> elt -> ('a * elt list)) -> 'a -> t val fold_map_right : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
(* map the element of the list from the last to the first. (* map the element of the list from the last to the first.
A memoisation is performed at each step *) A memoisation is performed at each step *)
val fold_map_left : ('a -> elt -> ('a * elt list)) -> 'a -> t val fold_map_left : ('a -> elt1 -> ('a * elt2 list)) -> 'a -> (elt1,elt2) t
(* map the element of the list without an environnment. (* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *) A memoisation is performed at each step, and for each elements *)
val elt : (elt -> elt list) -> t val elt : (elt1 -> elt2 list) -> (elt1,elt2) 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 end
module Make : functor (X : Sig) -> S with type elt = X.t open Theory
module TDecl : S with type elt1 = decl and type elt2 = decl
(*module TDecl_or_Use : S with type elt1 = decl_or_use and type elt2 = decl_or_use*)
module TTheory : S with type elt1 = theory and type elt2 = theory
module TTheory_Decl : S with type elt1 = theory and type elt2 = decl
module TDecl : S with type elt = Theory.decl
module TDecl_or_Use : S with type elt = Theory.decl_or_use