Commit fb157f53 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

asymmetric connetives put the label over the LHS formula

this is a tentative patch to make && and || more robust
wrt propositional simplification.
parent f80668a1
......@@ -185,9 +185,7 @@ let prio_binop = function
| Timplies -> 1
| Tiff -> 1
let print_label fmt l =
fprintf fmt "\"%s\"" l.lab_string
let print_label fmt l = fprintf fmt "\"%s\"" l.lab_string
let print_labels = print_iter1 Slab.iter space print_label
let print_loc fmt l =
......@@ -276,7 +274,7 @@ and print_tnode pri fmt t = match t.t_node with
| Tfalse ->
fprintf fmt "false"
| Tbinop (b,f1,f2) ->
let asym = Slab.mem Term.asym_label t.t_label in
let asym = Slab.mem Term.asym_label f1.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "@[<hov 1>%a %a@ %a@]")
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
......
......@@ -777,10 +777,9 @@ let t_implies = t_binary Timplies
let t_iff = t_binary Tiff
let asym_label = create_label "asym_split"
let asym_labels = Slab.singleton asym_label
let t_and_asym t1 t2 = t_label asym_labels (t_and t1 t2)
let t_or_asym t1 t2 = t_label asym_labels (t_or t1 t2)
let t_and_asym t1 t2 = t_and (t_label_add asym_label t1) t2
let t_or_asym t1 t2 = t_or (t_label_add asym_label t1) t2
(* closing constructors *)
......
......@@ -587,11 +587,11 @@ lexpr:
| lexpr OR lexpr
{ infix_pp $1 PPor $3 }
| lexpr BARBAR lexpr
{ mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPor $3)) }
{ infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPor $3 }
| lexpr AND lexpr
{ infix_pp $1 PPand $3 }
| lexpr AMPAMP lexpr
{ mk_pp (PPnamed (Lstr Term.asym_label, infix_pp $1 PPand $3)) }
{ infix_pp (mk_pp (PPnamed (Lstr Term.asym_label, $1))) PPand $3 }
| NOT lexpr
{ prefix_pp PPnot $2 }
| lexpr EQUAL lexpr
......
......@@ -215,7 +215,7 @@ and print_tnode pri fmt t = match t.t_node with
| Tfalse ->
fprintf fmt "false"
| Tbinop (b,f1,f2) ->
let asym = Slab.mem Term.asym_label t.t_label in
let asym = Slab.mem Term.asym_label f1.t_label in
let p = prio_binop b in
fprintf fmt (protect_on (pri > p) "%a %a@ %a")
(print_lterm (p + 1)) f1 (print_binop ~asym) b (print_lterm p) f2
......
......@@ -54,7 +54,7 @@ let rec split_pos ro acc f = match f.t_node with
| Ttrue -> acc
| Tfalse -> f::acc
| Tapp _ -> f::acc
| Tbinop (Tand,f1,f2) when asym f ->
| Tbinop (Tand,f1,f2) when asym f1 ->
split_pos ro (split_pos ro acc (t_implies f1 f2)) f1
| Tbinop (Tand,f1,f2) ->
split_pos ro (split_pos ro acc f2) f1
......@@ -101,7 +101,7 @@ and split_neg ro acc f = match f.t_node with
| Tbinop (Tand,f1,f2) ->
let fn f1 f2 = t_label_copy f (t_and f1 f2) in
apply_append2 fn acc (split_neg ro [] f1) (split_neg ro [] f2)
| Tbinop (Timplies,f1,f2) when asym f ->
| Tbinop (Timplies,f1,f2) when asym f1 ->
split_neg ro (split_neg ro acc (t_and f1 f2)) (t_not f1)
| Tbinop (Timplies,f1,f2) ->
split_neg ro (split_neg ro acc f2) (t_not f1)
......@@ -109,7 +109,7 @@ and split_neg ro acc f = match f.t_node with
let f12 = t_label_copy f (t_and f1 f2) in
let f21 = t_label_copy f (t_and (t_not f1) (t_not f2)) in
split_neg ro (split_neg ro acc f21) f12
| Tbinop (Tor,f1,f2) when asym f ->
| Tbinop (Tor,f1,f2) when asym f1 ->
split_neg ro (split_neg ro acc (t_and (t_not f1) f2)) f1
| Tbinop (Tor,f1,f2) ->
split_neg ro (split_neg ro acc f2) f1
......@@ -183,7 +183,7 @@ let rec split_intro pr dl acc f =
let rsp = split_intro pr dl in
match f.t_node with
| Ttrue -> acc
| Tbinop (Tand,f1,f2) when asym f ->
| Tbinop (Tand,f1,f2) when asym f1 ->
rsp (rsp acc (t_implies f1 f2)) f1
| Tbinop (Tand,f1,f2) ->
rsp (rsp acc f2) f1
......
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