Commit 4e3490c3 authored by Francois Bobot's avatar Francois Bobot

Mise à jour de transform, inlining,flatten,... cependant anomalie car un use...

Mise à jour de transform, inlining,flatten,... cependant anomalie car un use peut être ajouté par add_decl...
parent 84d9769a
......@@ -566,6 +566,7 @@ module Context = struct
let d = create_clone (Hid.fold add id_table []) in
push_decl ctxt d
let add_clone ctxt th inst =
let add_decl ctxt d = match d.d_node with
| Dtype _ | Dlogic _ | Dprop _ -> add_decl ctxt d
......
......@@ -128,8 +128,10 @@ module Context : sig
val use_export : context -> theory -> context
val clone_export : context -> theory -> th_inst -> context
val ctxt_fold : ('a -> decl -> 'a) -> 'a -> context -> 'a
val ctxt_fold : ('a -> decl -> 'a) -> 'a -> context -> 'a
(** bottom-up, tail-rec *)
val ctxt_iter : (decl -> unit) -> context -> unit
(** bottom-up, tail-rec *)
val get_decls : context -> decl list (* top-down list of decls *)
......
......@@ -17,84 +17,20 @@
(* *)
(**************************************************************************)
(* This module has the invariant that each type has only one tag function *)
type 'a hashconsedlist = (int * 'a list) list
type 'a tag = 'a -> int
module type Sig =
sig
type t
val tag : t tag
end
(* The datastructure for hashconsed list *)
module LH (X:Sig) =
struct
module L =
struct
type t = X.t hashconsedlist
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
| (_,[])::_,_ | _,(_,[])::_ -> assert false
let hash a =
match a with
| [] -> 0
| (_,[ae])::[] -> X.tag ae
| _::[] -> assert false
| (_,ae::_)::(at,_)::_ -> Hashcons.combine (X.tag ae) at
| (_,[])::_ -> assert false
let tag t = function
| [] -> []
| (_,lae)::al -> (t,lae)::al
end
module LH = Hashcons.Make(L)
type t = L.t
let empty : t = []
let cons e l : t = match l with
| [] -> LH.hashcons ([0,[e]])
| (_,l2)::_ -> LH.hashcons ((0,e::l2)::l)
let to_list t : X.t list = match t with
| [] -> []
| (_,l)::_ -> l
let from_list = List.fold_left (fun t e -> cons e t) empty
let fold_left f acc l =
List.fold_left (fun acc l -> match l with
| [] -> acc
| (tag,ae::_)::_ -> f acc tag ae
| (_,[])::_ -> assert false) acc l
let tag = function
| [] -> -1
| (t,_)::_ -> t
end
open Theory
open Context
(* 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}
type t = { all : context -> context;
clear : 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}
}
let apply f x = (List.rev (f.to_list (f.all (f.from_list x))))
let apply f x = f.all x
let clear f = f.clear ()
......@@ -105,111 +41,69 @@ let memo f tag h x =
Hashtbl.add h (tag x) r;
r
let d_tag d = d.d_tag
let ctxt_tag c = c.ctxt_tag
let t all clear clearf =
{all = all;
clear = match clear with
| None -> clearf
| Some clear -> (fun () -> clear ();clear ())
}
let fold_map_up ?clear f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind ecdone todo =
let _,ctxt_done = List.fold_left
(fun (env_done,ctxt_done) (desc,ctxt) ->
let ecdone = f_fold ctxt env_done ctxt_done desc in
Hashtbl.add memo_t ctxt.ctxt_tag ecdone;
ecdone) ecdone todo in
ctxt_done in
let rec f todo ctxt =
match ctxt.ctxt_decls with
| None -> rewind (v_empty,empty_context) todo
| Some (decls,ctxt2) ->
try
let ecdone = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind ecdone todo
with Not_found -> f ((decls,ctxt)::todo) ctxt2
in
t (f []) clear (fun () -> Hashtbl.clear memo_t)
let elt ?clear f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt _ () ctx x = (),
List.fold_left add_decl ctx (memo f_elt d_tag memo_elt x) in
let f = fold_map_up ?clear f_elt () in
{f with clear = fun () -> Hashtbl.clear memo_elt; f.clear ()}
let fold_map_bottom ?tag ?clear f_fold v_empty =
let rewind ldone ctxt =
List.fold_left (List.fold_left add_decl) ctxt ldone in
let tag_clear,tag_memo = match tag with
| None -> (fun () -> ()), (fun f ldone v ctxt -> f ldone v ctxt)
| Some tag_env ->
let memo_t = Hashtbl.create 64 in
(fun () -> Hashtbl.clear memo_t),(fun f ldone v ctxt ->
try
let ctxt = Hashtbl.find memo_t (ctxt.ctxt_tag,tag_env v) in
rewind ldone ctxt
with Not_found ->
let r = f ldone v ctxt in
Hashtbl.add memo_t (ctxt.ctxt_tag,tag_env v) r;
r
) in
let rec f ldone v ctxt =
match ctxt.ctxt_decls with
| None -> rewind ldone ctxt
| Some(d,ctxt2) ->
let v,res = f_fold ctxt v d in
tag_memo f (res::ldone) v ctxt2 in
let memo_t = Hashtbl.create 16 in
t (memo (f [] v_empty) ctxt_tag memo_t) clear (fun () -> tag_clear ();Hashtbl.clear memo_t)
let all ?clear f =
let memo_t = Hashtbl.create 16 in
t (memo f ctxt_tag memo_t) clear (fun () -> Hashtbl.clear memo_t)
module type S =
sig
type t1
type t2
val all : (t1 list -> t2 list) -> (t1,t2) t
val fold_map_right : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
val fold_map_left : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
val elt : (t1 -> t2 list) -> (t1,t2) t
end
module Make (X1 : Sig) (X2 : Sig) =
struct
type t1 = X1.t
type t2 = 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
}
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 -> LH2.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 (LH2.empty,v_empty) acc
| (_,[])::_ -> assert false
| (tag,e::_)::t2 ->
try
let edonev = Hashtbl.find memo_t tag in
rewind edonev acc
with Not_found -> f ((tag,e)::acc) t2
in
t (f []) (fun () -> Hashtbl.clear memo_t)
let elt f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt () x = (),memo f_elt X1.tag 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 -> LH2.cons e t)) LH2.empty acc
| (_,[])::_ -> assert false
| (_,e::_)::t ->
let v,res = f_fold v e in
f (res::acc,v) t in
let memo_t = Hashtbl.create 16 in
t (memo (f ([],v_empty)) LH1.tag memo_t) (fun () -> Hashtbl.clear memo_t)
let all f =
let f x = LH2.from_list (f (LH1.to_list x)) in
let memo_t = Hashtbl.create 16 in
t (memo f LH1.tag memo_t) (fun () -> Hashtbl.clear memo_t)
end
open Term
open Ty
open Theory
module SDecl =
struct
type t = decl
let tag x = x.d_tag
end
module STheory =
struct
type t = theory
let tag t = t.th_name.Ident.id_tag
end
module STerm =
struct
type t = Term.term
let tag t = t.Term.t_tag
end
module SFmla =
struct
type t = Term.fmla
let tag t = t.Term.f_tag
end
module TDecl = Make(SDecl)(SDecl)
module TTheory = Make(STheory)(STheory)
module TTheory_Decl = Make(STheory)(SDecl)
......@@ -17,69 +17,45 @@
(* *)
(**************************************************************************)
open Theory
(* Tranformation on list of element with some memoisations *)
(* The type of transformation from list of 'a to list of 'b *)
type ('a,'b) t
type t
(* compose two transformation, the underlying datastructures for
the memoisation are shared *)
val compose : ('a,'b) t -> ('b,'c) t -> ('a,'c) t
val compose : t -> t -> t
(* apply a transformation and memoise *)
val apply : ('a,'b) t -> 'a list -> 'b list
val apply : t -> context -> context
(* clear the datastructures used to store the memoisation *)
val clear : ('a,'b) t -> unit
(* The signature of a module of transformation from elt1 to elt2*)
module type S =
sig
(* The type of the elements of the list*)
type t1
type t2
(* The general tranformation only one memoisation is performed with
the argument given *)
val all : (t1 list -> t2 list) -> (t1,t2) t
(* map the element of the list from the first to the last.
only one memoisation is performed *)
val fold_map_right : ('a -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) 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 -> t1 -> ('a * t2 list)) -> 'a -> (t1,t2) t
(* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *)
val elt : (t1 -> t2 list) -> (t1,t2) t
end
(* a type with a tag function *)
type 'a tag
module type Sig =
sig
type t
val tag : t tag
end
open Theory
open Term
(* They are the only modules of signature S, we can have *)
module STerm : Sig with type t = term
module SFmla : Sig with type t = fmla
module SDecl : Sig with type t = decl
module STheory : Sig with type t = theory
(* The functor to construct transformation from one S.t to another *)
module Make (X1 : Sig)(X2 : Sig) : S with type t1 = X1.t with type t2 = X2.t
(* Predefined transformation *)
module TDecl : S with type t1 = decl and type t2 = decl
module TTheory : S with type t1 = theory and type t2 = theory
module TTheory_Decl : S with type t1 = theory and type t2 = decl
val clear : t -> unit
(* The general tranformation only one memoisation is performed with
the argument given *)
val all :
?clear:(unit -> unit) ->
(context -> context) -> t
(* map the element of the list from the first to the last.
only one memoisation is performed. But if a tag function is given.
A memoisation is performed at each step *)
val fold_map_bottom :
?tag:('a -> int) ->
?clear:(unit -> unit) ->
(context -> 'a -> decl -> 'a * decl 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_up :
?clear:(unit -> unit) ->
(context -> 'a -> context -> decl -> ('a * context)) -> 'a -> t
(* map the element of the list without an environnment.
A memoisation is performed at each step, and for each elements *)
val elt :
?clear:(unit -> unit) ->
(decl -> decl list) -> t
......@@ -70,7 +70,7 @@ let transform l =
let l = Typing.list_theory l in
if !print_stdout && not transform then
List.iter (Pretty.print_theory Format.std_formatter) l
(* else
else
let l = List.map (fun t -> t,Transform.apply Flatten.t t.Theory.th_ctxt)
l in
let l = if !simplify_recursive
......@@ -86,9 +86,9 @@ let transform l =
List.iter (fun (t,dl) ->
Format.printf "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n@?"
Pretty.print_ident t.Theory.th_name
Pretty.print_decl_list dl
Pretty.print_context dl
) l
*)
let () =
try
......
......@@ -171,10 +171,11 @@ let print_decl fmt d = match d.d_node with
let print_decl_list fmt de =
fprintf fmt "@[<hov>%a@]" (print_list newline print_decl) de
let print_ctxt = print_iter1 Context.ctxt_iter newline print_decl
let print_context fmt ctxt = print_list newline print_decl fmt
(Context.get_decls ctxt)
let print_theory fmt t =
fprintf fmt "@[@[<hov 2>theory %a@\n%a@]@\nend@]@\n@\n" print_ident t.th_name
print_ctxt t.th_ctxt;
print_context t.th_ctxt;
fprintf fmt "@?"
......@@ -39,4 +39,6 @@ val print_decl : formatter -> decl -> unit
val print_decl_list : formatter -> decl list -> unit
val print_context : formatter -> context -> unit
val print_theory : formatter -> theory -> unit
open Theory
(* Il faut supprimer les goals et transformer les lemmes en axioms *)
let elt a =
let rec aux acc d = match d.d_node with
| Duse t -> Context.ctxt_fold aux (d::acc) t.th_ctxt
let rec aux first_level acc d = match first_level, d.d_node with
| _,Duse t -> Context.ctxt_fold (aux false) (d::acc) t.th_ctxt
| false,Dprop (Pgoal,_,_) -> acc
| false,Dprop (Plemma,i,f) -> (create_prop Paxiom (Ident.id_dup i) f)::acc
| _ -> d::acc
in List.rev (aux [] a)
in
(* Pourquoi ce rev? *)
let r = (aux true [] a) in
Format.printf "flat %a : %a@\n" Pretty.print_decl a Pretty.print_decl_list r;
r
let t = Transform.TDecl.elt elt
let t = Transform.elt elt
(* a list of decl_or_use to a list of decl *)
val t : (Theory.decl,Theory.decl) Transform.t
val t : Transform.t
open Ident
open Term
open Theory
open Context
let ttrue _ = true
let ffalse _ = false
......@@ -46,30 +47,34 @@ and replacep env f =
and substt env d = t_map (replacet env) (replacep env) d
and substp env d = f_map (replacet env) (replacep env) d
let fold env d =
let fold _ env ctxt d =
Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;
match d.d_node with
| Dlogic [l] -> begin
match l with
| Lfunction (fs,None) -> env,[d]
| Lfunction (fs,None) -> env,add_decl ctxt d
| Lfunction (fs,Some fmla) ->
let _,vs,t = open_fs_defn fmla in
let t = replacet env t in
if t_s_any ffalse ((==) fs) t
then env,[create_logic [Lfunction(fs,Some (make_fs_defn fs vs t))]]
else {env with fs = Mls.add fs (vs,t) env.fs},[]
| Lpredicate (ps,None) -> env,[d]
then env,
add_decl ctxt (create_logic [Lfunction(fs,Some (make_fs_defn fs vs t))])
else {env with fs = Mls.add fs (vs,t) env.fs},ctxt
| Lpredicate (ps,None) -> env,add_decl ctxt d
| Lpredicate (ps,Some fmla) ->
let _,vs,f = open_ps_defn fmla in
let f = replacep env f in
if f_s_any ffalse ((==) ps) f
then env,[create_logic [Lpredicate(ps,Some (make_ps_defn ps vs f))]]
else {env with ps = Mls.add ps (vs,f) env.ps},[]
then env,
add_decl ctxt
(create_logic [Lpredicate(ps,Some (make_ps_defn ps vs f))])
else {env with ps = Mls.add ps (vs,f) env.ps},ctxt
| Linductive (ps,fmlal) ->
let fmlal = List.map (fun (id,fmla) -> id,replacep env fmla) fmlal in
env,[create_logic [Linductive (ps,fmlal)]]
env,add_decl ctxt (create_logic [Linductive (ps,fmlal)])
end
| Dlogic dl -> env,
[create_logic
add_decl ctxt (create_logic
(List.map
(function
| Lfunction (fs,None) as a -> a
......@@ -86,9 +91,9 @@ let fold env d =
let fmlal = List.map
(fun (id,fmla) -> id,replacep env fmla) fmlal in
Linductive (ps,fmlal)
) dl)]
| Dtype dl -> env,[d]
| Dprop (k,i,fmla) -> env,[create_prop k (id_dup i) (replacep env fmla)]
| Duse _ | Dclone _ -> env,[d]
) dl))
| Dtype dl -> env,add_decl ctxt d
| Dprop (k,i,fmla) -> env,add_decl ctxt (create_prop k (id_dup i) (replacep env fmla))
| Duse _ | Dclone _ -> env,add_decl ctxt d
let t = Transform.TDecl.fold_map_left fold empty_env
let t = Transform.fold_map_up fold empty_env
(* Inline the definition not recursive *)
val t : (Theory.decl,Theory.decl) Transform.t
val t : Transform.t
......@@ -146,4 +146,4 @@ let elt d =
List.map (fun e -> create_type (List.map (Hid.find mem) e)) l
| Dclone _ | Duse _ -> [d]
let t = Transform.TDecl.elt elt
let t = Transform.elt elt
......@@ -20,4 +20,4 @@
(* Simplify the recursive type and logic definition *)
val t : (Theory.decl,Theory.decl) Transform.t
val t : Transform.t
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