Commit 9c5072d4 authored by Andrei Paskevich's avatar Andrei Paskevich

split match statements in split_goal (without eliminating them)

parent 71b809e9
......@@ -24,6 +24,15 @@ 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 split_case spl c acc tl bl =
let bl = List.rev_map f_open_branch bl in
let bll,_ = List.fold_left (fun (bll,el) (pl,f) ->
let bll = List.rev_map (fun rl -> (pl,c)::rl) bll in
let bll = apply_append (fun f -> (pl,f)::el) bll (spl [] f) in
bll, (pl,c)::el) ([],[]) bl
in
apply_append (f_case tl) acc bll
let rec split_pos acc f = match f.f_node with
| Ftrue -> acc
| Ffalse -> f::acc
......@@ -42,7 +51,8 @@ let rec split_pos acc f = match f.f_node with
split_pos (split_pos acc (f_implies fif fthen)) (f_or fif felse)
| Flet (t,fb) -> let vs,f = f_open_bound fb in
apply_append (f_let vs t) acc (split_pos [] f)
| Fcase _ -> (* TODO better *) f::acc
| Fcase (tl,bl) ->
split_case split_pos f_true acc tl bl
| Fquant (Fforall,fq) -> let vsl,trl,f = f_open_quant fq in
(* TODO : Remove unused variable *)
apply_append (f_forall vsl trl) acc (split_pos [] f)
......@@ -66,7 +76,8 @@ and split_neg acc f = match f.f_node with
split_neg (split_neg acc (f_and fif fthen)) (f_and (f_not fif) felse)
| Flet (t,fb) -> let vs,f = f_open_bound fb in
apply_append (f_let vs t) acc (split_neg [] f)
| Fcase _ -> (* TODO better *) f::acc
| Fcase (tl,bl) ->
split_case split_neg f_false acc tl bl
| Fquant (Fexists,fq) -> let vsl,trl,f = f_open_quant fq in
(* TODO : Remove unused variable *)
apply_append (f_exists vsl trl) acc (split_neg [] f)
......
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