From aad1daa4e46956bdd3c24cae8558e7df5e0cd0f5 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sun, 28 Nov 2021 13:36:19 -0500 Subject: [PATCH] feat(quip): remove lit and not-normalization from quip --- src/base/Proof_quip.ml | 4 ++-- src/quip/Proof.ml | 20 +++++--------------- src/quip/Sidekick_quip.ml | 6 +++--- 3 files changed, 10 insertions(+), 20 deletions(-) diff --git a/src/base/Proof_quip.ml b/src/base/Proof_quip.ml index 58e34f1b..e4525c73 100644 --- a/src/base/Proof_quip.ml +++ b/src/base/Proof_quip.ml @@ -220,7 +220,7 @@ end = struct let name = name_clause lid in let step = lazy ( - let c = P.nn @@ L_proofs.find c in + let c = L_proofs.find c in let using = Util.array_to_list_map L_proofs.find using in let res = !! res in P.S_step_c {name; res; proof=P.Clause_rw {res; c0=c; using}} @@ -242,7 +242,7 @@ end = struct Array.iter add_needed_step exprs; let p = lazy ( let exprs = Util.array_to_list_map L_terms.find exprs in - P.nn @@ P.bool_c rule exprs + P.bool_c rule exprs ) in L_proofs.add lid p; diff --git a/src/quip/Proof.ml b/src/quip/Proof.ml index 40533471..a433bdcb 100644 --- a/src/quip/Proof.ml +++ b/src/quip/Proof.ml @@ -77,27 +77,19 @@ type ty = Ty.t module Lit = struct type t = - | L_eq of bool * term * term + | L_eq of term * term | L_a of bool * term - let not = function - | L_eq (sign,a,b) -> L_eq(not sign,a,b) - | L_a (sign,t) -> L_a (not sign,t) - let pp_with ~pp_t out = - let strsign = function true -> "+" | false -> "-" in function - | L_eq (b,t,u) -> Fmt.fprintf out "(@[%s@ (@[=@ %a@ %a@])@])" (strsign b) pp_t t pp_t u - | L_a (b,t) -> Fmt.fprintf out "(@[%s@ %a@])" (strsign b) pp_t t + | L_eq (t,u) -> Fmt.fprintf out "(@[=@ %a@ %a@])" pp_t t pp_t u + | L_a (false,t) -> Fmt.fprintf out "(@[not@ %a@])" pp_t t + | L_a (true,t) -> pp_t out t let pp = pp_with ~pp_t:T.pp - let a t = L_a (true,t) - let na t = L_a (false,t) - let eq t u = L_eq (true,t,u) - let neq t u = L_eq (false,t,u) + let eq t u = L_eq (t,u) let mk b t = L_a (b,t) - let sign = function L_a (b,_) | L_eq (b,_,_) -> b end type clause = Lit.t list @@ -129,7 +121,6 @@ type t = | Bool_true_neq_false | Bool_eq of term * term (* equal by pure boolean reasoning *) | Bool_c of bool_c_name * term list (* boolean tautology *) - | Nn of t (* negation normalization *) | Ite_true of term (* given [if a b c] returns [a=T |- if a b c=b] *) | Ite_false of term | LRA of clause @@ -205,7 +196,6 @@ let true_is_true : t = Bool_true_is_true let true_neq_false : t = Bool_true_neq_false let bool_eq a b : t = Bool_eq (a,b) let bool_c name c : t = Bool_c (name, c) -let nn c : t = Nn c let hres_l p l : t = let l = List.filter (function (P1 (Refl _)) -> false | _ -> true) l in diff --git a/src/quip/Sidekick_quip.ml b/src/quip/Sidekick_quip.ml index ad50f249..21f17b99 100644 --- a/src/quip/Sidekick_quip.ml +++ b/src/quip/Sidekick_quip.ml @@ -60,8 +60,9 @@ module Make_printer(Out : OUT) = struct let pp_l ppx xs = l (List.map ppx xs) let pp_lit ~pp_t lit = match lit with - | Lit.L_a(b,t) -> l[a(if b then"+" else"-");pp_t t] - | Lit.L_eq(b,t,u) -> l[a(if b then"+" else"-");l[a"=";pp_t t;pp_t u]] + | Lit.L_a(true,t) -> pp_t t + | Lit.L_a(false,t) -> l[a"not";pp_t t] + | Lit.L_eq(t,u) -> l[a"=";pp_t t;pp_t u] let pp_cl ~pp_t c = l (a "cl" :: List.map (pp_lit ~pp_t) c) @@ -80,7 +81,6 @@ module Make_printer(Out : OUT) = struct | Bool_true_neq_false -> a"t-ne-f" | Bool_eq (t1,t2) -> l[a"bool-eq";pp_t t1;pp_t t2] | Bool_c (name,ts) -> l(a"bool-c" :: a name :: List.map pp_t ts) - | Nn p -> l[a"nn";pp_rec p] | Assertion t -> l[a"assert";pp_t t] | Assertion_c c -> l[a"assert-c";pp_cl c] | Hres (c, steps) -> l[a"hres";pp_rec c;l(List.map pp_hres_step steps)]