Commit aff41e65 authored by Andrei Paskevich's avatar Andrei Paskevich

"Ouaaaaais" commit

Update the whole shebang to use the new core modules
parent 6aacb69c
......@@ -128,7 +128,7 @@ PARSER_CMO := parser.cmo lexer.cmo typing.cmo
PARSER_CMO := $(addprefix src/parser/,$(PARSER_CMO))
TRANSFORM_CMO := simplify_recursive_definition.cmo inlining.cmo\
split_conjunction.cmo split_goals.cmo
split_conjunction.cmo
TRANSFORM_CMO := $(addprefix src/transform/,$(TRANSFORM_CMO))
DRIVER_CMO := call_provers.cmo dynlink_compat.cmo driver_parser.cmo\
......
......@@ -23,7 +23,9 @@ open Util
open Ident
open Ty
open Term
open Theory
open Decl
open Theory2
open Task
let iprinter,tprinter,lprinter,pprinter =
let bl = ["theory"; "type"; "logic"; "inductive";
......@@ -327,22 +329,26 @@ let print_decl fmt d = match d.d_node with
| Dlogic ll -> print_list newline print_logic_decl fmt ll
| Dind il -> print_list newline print_ind_decl fmt il
| Dprop p -> print_prop_decl fmt p
| Duse th ->
let print_tdecl fmt = function
| Decl d ->
print_decl fmt d
| Use th ->
fprintf fmt "@[<hov 2>(* use %a *)@]" print_th th
| Dclone (th,inst) ->
| Clone (th,inst) ->
fprintf fmt "@[<hov 2>(* clone %a with %a *)@]"
print_th th (print_list comma print_inst) inst
let print_decls fmt dl =
fprintf fmt "@[<hov>%a@\n@]" (print_list newline2 print_decl) dl
let print_context fmt ctxt = print_decls fmt (Context.get_decls ctxt)
let print_task fmt task = print_decls fmt (task_decls task)
let print_theory fmt th =
fprintf fmt "@[<hov 2>theory %a@\n%a@]@\nend@\n@."
print_th th print_context th.th_ctxt
print_th th (print_list newline2 print_tdecl) th.th_decls
let print_named_context fmt name ctxt =
fprintf fmt "@[<hov 2>context %s@\n%a@]@\nend@\n@."
name print_context ctxt
let print_named_task fmt name task =
fprintf fmt "@[<hov 2>task %s@\n%a@]@\nend@\n@."
name print_task task
......@@ -21,7 +21,9 @@ open Format
open Ident
open Ty
open Term
open Theory
open Decl
open Theory2
open Task
val forget_all : unit -> unit (* flush id_unique *)
val forget_tvs : unit -> unit (* flush id_unique for type vars *)
......@@ -52,8 +54,8 @@ val print_prop_decl : formatter -> prop_decl -> unit
val print_decl : formatter -> decl -> unit
val print_decls : formatter -> decl list -> unit
val print_context : formatter -> context -> unit
val print_task : formatter -> task -> unit
val print_theory : formatter -> theory -> unit
val print_named_context : formatter -> string -> context -> unit
val print_named_task : formatter -> string -> task -> unit
......@@ -17,7 +17,6 @@
(* *)
(**************************************************************************)
open Format
open Util
open Ident
open Ty
......@@ -48,8 +47,6 @@ let add_clone =
incr r;
{ cl_map = merge_clone cl.cl_map th sl; cl_tag = !r }
let clone_tag cl = cl.cl_tag
(** Known identifiers *)
......@@ -170,10 +167,16 @@ let mk_task decl prev known = Htask.hashcons {
task_tag = -1;
}
exception GoalFound
let push_decl task d =
try
let kn = add_decl task.task_known d in
ignore (check_decl kn d);
begin match task.task_decl.d_node with
| Dprop (Pgoal,_,_) -> raise GoalFound
| _ -> ()
end;
mk_task d (Some task) kn
with DejaVu -> task
......@@ -232,14 +235,11 @@ let rec use_export names acc td =
used, cl, res, push_decl task d
end
let split_theory_opt th names =
let split_theory th names =
let acc = Sid.empty, empty_clone, [], of_option init_task in
let _, _, res, _ = List.fold_left (use_export names) acc th.th_decls in
res
let split_theory th names = split_theory_opt th (Some names)
let split_theory_full th = split_theory_opt th None
(* Generic utilities *)
let rec task_fold fn acc = function
......@@ -258,116 +258,3 @@ let task_goal = function
| Some { task_decl = { d_node = Dprop (Pgoal,pr,_) }} -> pr
| _ -> raise GoalNotFound
(** Task transformation *)
module Tr = struct
type 'a trans = task -> 'a
type 'a tlist = 'a list trans
let identity x = x
let identity_l x = [x]
let conv_res f c x = c (f x)
let singleton f x = [f x]
let compose f g x = g (f x)
let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
let compose_l f g x = list_apply g (f x)
let apply f x = f x
let ymemo f tag h =
let rec aux x =
let t = tag x in
try
Hashtbl.find h t
with Not_found ->
let r = f aux x in
Hashtbl.add h t r;
r in
aux
let memo f tag h = ymemo (fun _ -> f) tag h
let term_tag t = t.t_tag
let fmla_tag f = f.f_tag
let decl_tag d = d.d_tag
let task_tag = function
| Some t -> t.task_tag
| None -> -1
let store f = memo f task_tag (Hashtbl.create 63)
let accum memo_t rewind v =
let rec accum todo = function
| Some task ->
let curr =
try Some (Hashtbl.find memo_t task.task_tag)
with Not_found -> None
in
begin match curr with
| Some curr -> rewind curr todo
| None -> accum (task::todo) task.task_prev
end
| None -> rewind v todo
in
accum
let save memo_t task v = Hashtbl.add memo_t task.task_tag v; v
let fold fn v =
let memo_t = Hashtbl.create 63 in
let rewind x task = save memo_t task (fn task x) in
let rewind = List.fold_left rewind in
accum memo_t rewind v []
let fold_l fn v =
let memo_t = Hashtbl.create 63 in
let rewind x task = save memo_t task (list_apply (fn task) x) in
let rewind = List.fold_left rewind in
accum memo_t rewind [v] []
let fold_map fn v = conv_res (fold fn (v, None)) snd
let fold_map_l fn v = conv_res (fold_l fn (v, None)) (List.rev_map snd)
let map fn = fold (fun t1 t2 -> fn t1 t2) None
let map_l fn = fold_l (fun t1 t2 -> fn t1 t2) None
let decl fn =
let memo_t = Hashtbl.create 63 in
let fn task = memo fn decl_tag memo_t task.task_decl in
let fn task acc = List.fold_left add_decl acc (fn task) in
map fn
let decl_l fn =
let memo_t = Hashtbl.create 63 in
let fn task = memo fn decl_tag memo_t task.task_decl in
let fn task acc = List.rev_map (List.fold_left add_decl acc) (fn task) in
map_l fn
let rewrite fnT fnF d = match d.d_node with
| Dtype _ ->
d
| Dlogic l ->
let fn = function
| ls, Some ld ->
let vl,e = open_ls_defn ld in
make_ls_defn ls vl (e_map fnT fnF e)
| ld -> ld
in
create_logic_decl (List.map fn l)
| Dind l ->
let fn (pr,f) = pr, fnF f in
let fn (ps,l) = ps, List.map fn l in
create_ind_decl (List.map fn l)
| Dprop (k,pr,f) ->
create_prop_decl k pr (fnF f)
let expr fnT fnF = decl (fun d -> [rewrite fnT fnF d])
end
......@@ -25,12 +25,13 @@ open Theory2
(** Cloning map *)
type clone
type clone = private {
cl_map : clone_map;
cl_tag : int
}
val cloned_from : clone -> ident -> ident -> bool
val clone_tag : clone -> int
(** Task *)
type task = task_hd option
......@@ -44,14 +45,9 @@ and task_hd = private {
(* constructors *)
(* val init_task : task *)
(* val add_decl : task -> decl -> task *)
val add_decl : task -> decl -> task
val split_theory : theory -> Spr.t -> (task * clone) list
val split_theory_full : theory -> (task * clone) list
val split_theory : theory -> Spr.t option -> (task * clone) list
(* bottom-up, tail-recursive traversal functions *)
......@@ -68,43 +64,5 @@ val task_goal : task -> prop
exception UnknownIdent of ident
exception RedeclaredIdent of ident
exception GoalNotFound
(** Task transformation *)
module Tr : sig
type 'a trans
type 'a tlist = 'a list trans
val identity : task trans
val identity_l : task tlist
val apply : 'a trans -> (task -> 'a)
val store : (task -> 'a) -> 'a trans
val singleton : 'a trans -> 'a tlist
val compose : task trans -> 'a trans -> 'a trans
val compose_l : task tlist -> 'a tlist -> 'a tlist
(* val conv_res : 'a trans -> ('a -> 'b) -> 'b trans *)
val fold : (task_hd -> 'a -> 'a ) -> 'a -> 'a trans
val fold_l : (task_hd -> 'a -> 'a list) -> 'a -> 'a tlist
val fold_map :
(task_hd -> 'a * task -> ('a * task) ) -> 'a -> task trans
val fold_map_l :
(task_hd -> 'a * task -> ('a * task) list) -> 'a -> task tlist
val map : (task_hd -> task -> task ) -> task trans
val map_l : (task_hd -> task -> task list) -> task tlist
val decl : (decl -> decl list ) -> task trans
val decl_l : (decl -> decl list list) -> task tlist
val expr : (term -> term) -> (fmla -> fmla) -> task trans
end
exception GoalFound
......@@ -27,8 +27,8 @@ open Decl
(** Namespace *)
module Snm = Set.Make(String)
module Mnm = Map.Make(String)
module Snm = Sstr
module Mnm = Mstr
type namespace = {
ns_ts : tysymbol Mnm.t; (* type symbols *)
......
......@@ -17,47 +17,41 @@
(* *)
(**************************************************************************)
open Term
open Util
open Ident
open Theory
open Context
open Ty
open Term
open Termlib
open Decl
open Theory2
open Task
(* the memoisation is inside the function *)
type 'a t = {
all : context -> 'a;
clear : unit -> unit;
}
(** Task transformation *)
type ctxt_t = context t
type ctxt_list_t = context list t
type 'a trans = task -> 'a
type 'a tlist = 'a list trans
let conv_res f c =
{ all = (fun x -> c (f.all x));
clear = f.clear; }
let identity x = x
let identity_l x = [x]
let compose f g =
{ all = (fun x -> g.all (f.all x));
clear = (fun () -> f.clear (); g.clear ()); }
let conv_res f c x = c (f x)
let compose' f g =
{ all = (fun x -> List.fold_left (fun acc l -> List.rev_append (g.all l) acc)
[] (f.all x));
clear = (fun () -> f.clear (); g.clear ()); }
let singleton f x = [f x]
let singleton f =
{ all = (fun x -> [f.all x]);
clear = f.clear}
let compose f g x = g (f x)
let apply f x = f.all x
let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
let clear f = f.clear ()
let compose_l f g x = list_apply g (f x)
let apply f x = f x
let ymemo f tag h =
let rec aux x =
let t = tag x in
try
try
Hashtbl.find h t
with Not_found ->
with Not_found ->
let r = f aux x in
Hashtbl.add h t r;
r in
......@@ -65,214 +59,83 @@ let ymemo f tag h =
let memo f tag h = ymemo (fun _ -> f) tag h
let d_tag d = d.d_tag
let ctxt_tag c = c.ctxt_tag
let t all clear_all =
{ all = all;
clear = clear_all; }
let register f =
let memo_t = Hashtbl.create 17 in
t (memo f ctxt_tag memo_t) (fun () -> Hashtbl.clear memo_t)
let fold f_fold v_empty =
let memo_t = Hashtbl.create 64 in
let rewind env todo =
List.fold_left
(fun env ctxt ->
let env = f_fold ctxt env in
Hashtbl.add memo_t ctxt.ctxt_tag env;
env)
env todo
in
let rec f todo ctxt =
match ctxt.ctxt_prev with
| None ->
rewind (v_empty ctxt.ctxt_env) todo
| Some ctxt2 ->
try
let env = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind env (ctxt :: todo)
with Not_found ->
f (ctxt :: todo) ctxt2
in
t (f []) (fun () -> Hashtbl.clear memo_t)
let fold' (f_fold:context -> 'a -> 'a list) v_empty =
let memo_t = Hashtbl.create 64 in
let rewind env todo =
List.fold_left
(fun env ctxt ->
let env = List.fold_left
(fun acc e -> List.rev_append (f_fold ctxt e) acc) [] env in
Hashtbl.add memo_t ctxt.ctxt_tag env;
env)
env todo
in
let rec f todo ctxt =
match ctxt.ctxt_prev with
| None ->
rewind [v_empty ctxt.ctxt_env] todo
| Some ctxt2 ->
try
let env = Hashtbl.find memo_t ctxt2.ctxt_tag in
rewind env (ctxt :: todo)
with Not_found ->
f (ctxt :: todo) ctxt2
in
t (f []) (fun () -> Hashtbl.clear memo_t)
let fold_map f_fold v_empty =
let v_empty env = v_empty env, init_context env in
conv_res (fold f_fold v_empty) snd
let fold_map' f_fold v_empty =
let v_empty env = v_empty env, init_context env in
conv_res (fold' f_fold v_empty) (List.map snd)
let map f_map =
fold (fun ctxt1 ctxt2 -> f_map ctxt1 ctxt2) init_context
let map' f_map =
fold' (fun ctxt1 ctxt2 -> f_map ctxt1 ctxt2) init_context
let map_concat f_elt =
let f_elt ctxt0 ctxt = List.fold_left add_decl ctxt (f_elt ctxt0) in
map f_elt
let map_concat' f_elt =
let f_elt ctxt0 ctxt = List.map (List.fold_left add_decl ctxt) (f_elt ctxt0) in
map' f_elt
let elt f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt ctxt0 = memo f_elt d_tag memo_elt ctxt0.ctxt_decl in
let f = map_concat f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_elt; f.clear () }
let elt' f_elt =
let memo_elt = Hashtbl.create 64 in
let f_elt ctxt0 = memo f_elt d_tag memo_elt ctxt0.ctxt_decl in
let f = map_concat' f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_elt; f.clear () }
let elt_env f_elt =
let f_elt env =
let memo_elt = Hashtbl.create 64 in
memo (f_elt env) d_tag memo_elt in
let memo_env = Hashtbl.create 2 in
let f_elt ctxt = (memo f_elt env_tag memo_env ctxt.ctxt_env) ctxt.ctxt_decl in
let f = map_concat f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_env; f.clear () }
let elt_env' f_elt =
let f_elt env =
let memo_elt = Hashtbl.create 64 in
memo (f_elt env) d_tag memo_elt in
let memo_env = Hashtbl.create 2 in
let f_elt ctxt = (memo f_elt env_tag memo_env ctxt.ctxt_env) ctxt.ctxt_decl in
let f = map_concat' f_elt in
{ f with clear = fun () -> Hashtbl.clear memo_env; f.clear () }
(* Utils *)
(*type odecl =
| Otype of ty_decl
| Ologic of logic_decl
| Oprop of prop_decl
| Ouse of theory
| Oclone of (ident * ident) list*)
let elt_of_oelt ~ty ~logic ~ind ~prop ~use ~clone d =
match d.d_node with
| Dtype l -> [create_ty_decl (List.map ty l)]
| Dlogic l -> [create_logic_decl (List.map logic l)]
| Dind l -> ind l
| Dprop p -> prop p
| Duse th -> use th
| Dclone (th,c) -> clone th c
let fold_context_of_decl f ctxt env ctxt_done d =
let env,decls = f ctxt env d in
env,List.fold_left add_decl ctxt_done decls
let remove_lemma =
let f d =
match d.d_node with
| Dprop (Plemma, pr, f) ->
let da = create_prop_decl Paxiom pr f in
let dg = create_prop_decl Pgoal pr f in
[dg;da]
| _ -> [d]
let term_tag t = t.t_tag
let fmla_tag f = f.f_tag
let decl_tag d = d.d_tag
let task_tag = function
| Some t -> t.task_tag
| None -> -1
let store f = memo f task_tag (Hashtbl.create 63)
let accum memo_t rewind v =
let rec accum todo = function
| Some task ->
let curr =
try Some (Hashtbl.find memo_t task.task_tag)
with Not_found -> None
in
begin match curr with
| Some curr -> rewind curr todo
| None -> accum (task::todo) task.task_prev
end
| None -> rewind v todo
in
elt f
exception NotGoalContext
let goal_of_ctxt ctxt =
match ctxt.ctxt_decl.d_node with
| Dprop (Pgoal,pr,_) -> pr
| _ -> raise NotGoalContext
let identity =
{ all = (fun x -> x);
clear = (fun () -> ()); }
let identity' = singleton identity
let rewrite_elt rt rf d =
match d.d_node with
| Dtype _ -> [d]
| Dlogic l -> [create_logic_decl (List.map
(function
| (ls,Some def) ->
let vsl,expr = open_ls_defn def in
let expr = e_map rt rf expr in
make_ls_defn ls vsl expr
| l -> l) l)]
| Dind indl -> [create_ind_decl
(List.map (fun (ls,pl) -> ls,
(List.map (fun (pr,f) -> (pr, rf f)) pl)) indl)]
|Dprop (k,pr,f) -> [create_prop_decl k pr (rf f)]
|Duse _ |Dclone _ -> [d]
let rewrite_env rt rf env =
let rt = rt env in
let rf = rf env in
rewrite_elt rt rf
let rewrite_elt rt rf = elt (rewrite_elt rt rf)
accum
let save memo_t task v = Hashtbl.add memo_t task.task_tag v; v
let fold fn v =
let memo_t = Hashtbl.create 63 in
let rewind x task = save memo_t task (fn task x) in
let rewind = List.fold_left rewind in
accum memo_t rewind v []
let fold_l fn v =
let memo_t = Hashtbl.create 63 in
let rewind x task = save memo_t task (list_apply (fn task) x) in
let rewind = List.fold_left rewind in
accum memo_t rewind [v] []
let fold_map fn v = conv_res (fold fn (v, None)) snd
let fold_map_l fn v = conv_res (fold_l fn (v, None)) (List.rev_map snd)
let map fn = fold (fun t1 t2 -> fn t1 t2) None
let map_l fn = fold_l (fun t1 t2 -> fn t1 t2) None
let decl fn =
let memo_t = Hashtbl.create 63 in
let fn task = memo fn decl_tag memo_t task.task_decl in
let fn task acc = List.fold_left add_decl acc (fn task) in
map fn
let decl_l fn =