Commit 64452f73 authored by Andrei Paskevich's avatar Andrei Paskevich

conjunction and disjunction are right-associative

parent 021b6fcf
......@@ -1337,7 +1337,7 @@ let t_and_simp f1 f2 = match f1.t_node, f2.t_node with
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_and f1 f2
let t_and_simp_l l = List.fold_left t_and_simp t_true l
let t_and_simp_l l = List.fold_right t_and_simp l t_true
let t_or_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f2 -> t_label_remove asym_label f1
......@@ -1347,7 +1347,7 @@ let t_or_simp f1 f2 = match f1.t_node, f2.t_node with
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_or f1 f2
let t_or_simp_l l = List.fold_left t_or_simp t_false l
let t_or_simp_l l = List.fold_right t_or_simp l t_false
let t_and_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f1 -> f2
......@@ -1357,7 +1357,7 @@ let t_and_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_and_asym f1 f2
let t_and_asym_simp_l l = List.fold_left t_and_asym_simp t_true l
let t_and_asym_simp_l l = List.fold_right t_and_asym_simp l t_true
let t_or_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f2 -> t_label_remove asym_label f1
......@@ -1367,7 +1367,7 @@ let t_or_asym_simp f1 f2 = match f1.t_node, f2.t_node with
| _, _ when t_equal f1 f2 -> f1
| _, _ -> t_or_asym f1 f2
let t_or_asym_simp_l l = List.fold_left t_or_asym_simp t_false l
let t_or_asym_simp_l l = List.fold_right t_or_asym_simp l t_false
let t_implies_simp f1 f2 = match f1.t_node, f2.t_node with
| Ttrue, _ when can_simp f1 -> f2
......
......@@ -105,8 +105,8 @@ let rec cs_equ kn env t1 t2 =
and apply_cs_equ kn cs1 tl1 env t = match t.t_node with
| Tapp (cs2,tl2) when ls_equal cs1 cs2 ->
let merge f t1 t2 = t_and_simp f (cs_equ kn env t1 t2) in
List.fold_left2 merge t_true tl1 tl2
let merge t1 t2 f = t_and_simp (cs_equ kn env t1 t2) f in
List.fold_right2 merge tl1 tl2 t_true
| Tapp _ -> t_false
| _ -> assert false
......
......@@ -23,6 +23,11 @@ let map_fold_left f acc l =
let acc, rev = rev_map_fold_left f acc l in
acc, List.rev rev
let map_fold_right f l acc =
List.fold_right
(fun e (l, acc) -> let e, acc = f e acc in e :: l, acc)
l ([], acc)
let equal pr l1 l2 =
try List.for_all2 pr l1 l2 with Invalid_argument _ -> false
......
......@@ -17,6 +17,9 @@ val rev_map_fold_left :
val map_fold_left :
('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
val map_fold_right :
('a -> 'acc -> 'b * 'acc) -> 'a list -> 'acc -> 'b list * 'acc
val equal : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
val compare : ('a -> 'a -> int) -> 'a list -> 'a list -> int
......
......@@ -234,14 +234,14 @@ let decrease_alg ?loc env old_t t =
let csl = Decl.find_constructors env.pure_known ts in
if csl = [] then quit ();
let sbs = ty_match Mtv.empty (ty_app ts (List.map ty_var ts.ts_args)) oty in
let add_arg acc fty =
let add_arg fty acc =
let fty = ty_inst sbs fty in
if ty_equal fty nty then
let vs = create_vsymbol (id_fresh "f") nty in
t_or_simp acc (t_equ (t_var vs) t), pat_var vs
else acc, pat_wild fty in
pat_var vs, t_or_simp (t_equ (t_var vs) t) acc
else pat_wild fty, acc in
let add_cs (cs,_) =
let f, pl = Lists.map_fold_left add_arg t_false cs.ls_args in
let pl, f = Lists.map_fold_right add_arg cs.ls_args t_false in
t_close_branch (pat_app cs pl oty) f in
t_case old_t (List.map add_cs csl)
......
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