Commit cdd7a8d1 authored by Andrei Paskevich's avatar Andrei Paskevich

put the proposed interface for transformations into Task.Tr

- env-dependent functions are not needed any more

- the member function [clear] is not needed, it is
  the responsibility of Driver to drop and recreate
  transformations whenever desirable. 
  
  (François, don't get mad, please :)
parent f0218f41
......@@ -251,3 +251,66 @@ let rec task_iter fn task =
let task_decls = task_fold (fun acc d -> d::acc) []
exception GoalNotFound
let task_goal task = match task.task_decl.d_node with
| 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 compose_l f g x =
List.fold_left (fun acc l -> List.rev_append (g l) acc) [] (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 t = t.task_tag
let store f = memo f task_tag (Hashtbl.create 63)
let fold fn v = assert false (* TODO *)
let fold_l fn v = assert false (* TODO *)
let fold_map fn v = conv_res (fold fn (v, init_task)) snd
let fold_map_l fn v = conv_res (fold_l fn (v, init_task)) (List.rev_map snd)
let map fn = fold (fun t1 t2 -> fn t1 t2) init_task
let map_l fn = fold_l (fun t1 t2 -> fn t1 t2) init_task
let decl fn = assert false (* TODO *)
let decl_l fn = assert false (* TODO *)
let expr fnT fnF d = assert false (* TODO *)
end
......@@ -58,8 +58,47 @@ val task_iter : (decl -> unit) -> task -> unit
val task_decls : task -> decl list
val task_goal : task -> prop
(* exceptions *)
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 -> 'a -> 'a ) -> 'a -> 'a trans
val fold_l : (task -> 'a -> 'a list) -> 'a -> 'a tlist
val fold_map : (task -> 'a * task -> ('a * task) ) -> 'a -> task trans
val fold_map_l : (task -> 'a * task -> ('a * task) list) -> 'a -> task tlist
val map : (task -> task -> task ) -> task trans
val map_l : (task -> 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
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