Commit 504c6ffb authored by MARCHE Claude's avatar MARCHE Claude
Browse files

fix ordering of goals for transformations producing severals goals

parent d87e4263
......@@ -82,11 +82,8 @@ let fold fn v =
let fold_l fn v = fold (fun task -> list_apply (fn task)) [v]
let fold_map fn v t = conv_res snd (fold fn (v, t))
let fold_map_l fn v t = conv_res (List.rev_map snd) (fold_l fn (v, t))
let map fn = fold (fun t1 t2 -> fn t1 t2)
let map_l fn = fold_l (fun t1 t2 -> fn t1 t2)
let fold_map fn v t = conv_res snd (fold fn (v, t))
let fold_map_l fn v t = conv_res (List.map snd) (fold_l fn (v, t))
let gen_decl add fn =
let fn = Wdecl.memoize 63 fn in
......@@ -94,15 +91,15 @@ let gen_decl add fn =
| Decl d -> List.fold_left add acc (fn d)
| _ -> add_tdecl acc task.task_decl
in
map fn
fold fn
let gen_decl_l add fn =
let fn = Wdecl.memoize 63 fn in
let fn task acc = match task.task_decl.td_node with
| Decl d -> List.rev_map (List.fold_left add acc) (fn d)
| Decl d -> List.map (List.fold_left add acc) (fn d)
| _ -> [add_tdecl acc task.task_decl]
in
map_l fn
fold_l fn
let decl = gen_decl add_decl
let decl_l = gen_decl_l add_decl
......@@ -114,26 +111,16 @@ let apply_to_goal fn d = match d.d_node with
| _ -> assert false
let gen_goal add fn =
let fn = Wdecl.memoize 5 (apply_to_goal fn) in
let rec pass task = match task with
let fn = Wdecl.memoize 5 (apply_to_goal fn) in function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.fold_left add prev (fn d)
| Some { task_decl = td; task_prev = prev } ->
add_tdecl (pass prev) td
| _ -> assert false
in
pass
let gen_goal_l add fn =
let fn = Wdecl.memoize 5 (apply_to_goal fn) in
let rec pass task = match task with
let fn = Wdecl.memoize 5 (apply_to_goal fn) in function
| Some { task_decl = { td_node = Decl d }; task_prev = prev } ->
List.rev_map (List.fold_left add prev) (fn d)
| Some { task_decl = td; task_prev = prev } ->
List.rev_map (fun task -> add_tdecl task td) (pass prev)
List.map (List.fold_left add prev) (fn d)
| _ -> assert false
in
pass
let goal = gen_goal add_decl
let goal_l = gen_goal_l add_decl
......
......@@ -50,11 +50,6 @@ val fold_map : (task_hd -> 'a * task -> ('a * task)) ->
val fold_map_l : (task_hd -> 'a * task -> ('a * task) list) ->
'a -> task -> task tlist
val map : (task_hd -> task -> task ) -> task -> task trans
(** [map] is the same as fold with 'a = task *)
val map_l : (task_hd -> task -> task list) -> task -> task tlist
val decl : (decl -> decl list ) -> task -> task trans
(** [decl f acc [d1;..;dn]] returns acc@f d1@..@f dn *)
val decl_l : (decl -> decl list list) -> task -> task tlist
......
......@@ -557,6 +557,7 @@ let split_unproved_goals () =
subgoals = [];
}
in
List.iter (fun t -> eprintf "%a@." Pretty.print_task t) subgoals;
goals_model#set ~row:split_row ~column:Model.index_column
(Model.Row_transformation tr);
g.Model.transformations <- tr :: g.Model.transformations;
......
......@@ -73,7 +73,6 @@ let event_handler () =
(*
eprintf "[Why thread] Scheduler.event_handler: got prover answer@.";
*)
(* TODO: update database *)
(* call GUI callback with argument [res] *)
!async (fun () -> callback res time output) ()
| Editor_exited callback ->
......@@ -86,7 +85,6 @@ let event_handler () =
let (callback,transf,task) = Queue.pop transf_queue in
Mutex.unlock queue_lock;
let subtasks : Task.task list = Trans.apply transf task in
(* TODO: update database *)
(* call GUI back given new subgoals *)
!async (fun () -> callback subtasks) ()
with Queue.Empty ->
......
......@@ -52,7 +52,7 @@ let comp t task =
| Decl d -> add_decl task (decl_map fnT fnF d)
| _ -> add_tdecl task t.task_decl
let compile_match = Trans.map comp None
let compile_match = Trans.fold comp None
(** Eliminate algebraic types and match statements *)
......
......@@ -21,8 +21,12 @@ open Ident
open Term
open Decl
let apply_append fn = List.fold_left (fun l e -> fn e :: l)
let apply_append2 fn = Util.list_fold_product (fun l e1 e2 -> fn e1 e2 :: l)
let apply_append fn acc l =
List.fold_left (fun l e -> fn e :: l) acc (List.rev l)
let apply_append2 fn acc l1 l2 =
Util.list_fold_product (fun l e1 e2 -> fn e1 e2 :: l)
acc (List.rev l1) (List.rev l2)
let split_case spl c acc tl bl =
let bl = List.rev_map f_open_branch bl in
......@@ -50,14 +54,14 @@ let rec split_pos acc f = match f.f_node with
| Fbinop (Fimplies,f1,f2) ->
apply_append2 f_implies acc (split_neg [] f1) (split_pos [] f2)
| Fbinop (Fiff,f1,f2) ->
split_pos (split_pos acc (f_implies f1 f2)) (f_implies f2 f1)
split_pos (split_pos acc (f_implies f2 f1)) (f_implies f1 f2)
| Fbinop (For,f1,f2) ->
apply_append2 f_or acc (split_pos [] f1) (split_pos [] f2)
| Fnot f ->
apply_append f_not acc (split_neg [] f)
| Fif (fif,fthen,felse) ->
split_pos (split_pos acc (f_implies fif fthen))
(f_implies (f_not fif) felse)
split_pos (split_pos acc (f_implies (f_not fif) felse))
(f_implies fif fthen)
| Flet (t,fb) -> let vs,f = f_open_bound fb in
apply_append (f_let_close vs t) acc (split_pos [] f)
| Fcase (tl,bl) ->
......@@ -78,7 +82,7 @@ and split_neg acc f = match f.f_node with
| Fbinop (Fimplies,f1,f2) ->
split_neg (split_neg acc f2) (f_not f1)
| Fbinop (Fiff,f1,f2) ->
split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f2 f1)
split_neg (split_neg acc (f_and (f_not f1) (f_not f2))) (f_and f1 f2)
| Fbinop (For,f1,f2) when to_split f ->
split_neg (split_neg acc (f_and (f_not f1) f2)) f1
| Fbinop (For,f1,f2) ->
......@@ -86,7 +90,7 @@ and split_neg acc f = match f.f_node with
| Fnot f ->
apply_append f_not acc (split_pos [] f)
| Fif (fif,fthen,felse) ->
split_neg (split_neg acc (f_and fif fthen)) (f_and (f_not fif) felse)
split_neg (split_neg acc (f_and (f_not fif) felse)) (f_and fif fthen)
| Flet (t,fb) -> let vs,f = f_open_bound fb in
apply_append (f_let_close vs t) acc (split_neg [] f)
| Fcase (tl,bl) ->
......
......@@ -65,7 +65,8 @@ let map_join_left map join = function
| x :: xl -> List.fold_left (fun acc x -> join acc (map x)) (map x) xl
| _ -> raise (Failure "map_join_left")
let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
let list_apply f l =
List.rev (List.fold_left (fun acc x -> List.rev_append (f x) acc) [] l)
let list_fold_product f acc l1 l2 =
List.fold_left
......@@ -79,7 +80,8 @@ let list_fold_product_l f acc ll =
let ll = List.rev ll in
let rec aux acc le = function
| [] -> f acc le
| l::ll -> List.fold_left (fun acc e -> aux acc (e::le) ll) acc l in
| l::ll -> List.fold_left (fun acc e -> aux acc (e::le) ll) acc l
in
aux acc [] ll
let list_compare cmp l1 l2 = match l1,l2 with
......
......@@ -54,6 +54,7 @@ val list_all2 : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val map_join_left : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'a list -> 'b
val list_apply : ('a -> 'b list) -> 'a list -> 'b list
(** [list_apply f [a1;..;an] returns (f a1)@...@(f an) *)
val list_fold_product :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
......
......@@ -17,7 +17,9 @@ theory TestInt
goal Test5: forall x:int. x <> 0 -> x*x > 0
goal Test6: 2+3 = 5 and forall x:int. x*x >= 0
goal Test6: 2+3 = 5 and (forall x:int. x*x >= 0)
goal Test7: 0 = 1 /\ 2 = 3 /\ 4 = 5 /\ 6 = 7
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