(* Title: Tools/Argo/argo_cc.ML Author: Sascha Boehme Author: Dmitriy Traytel and Matthias Franze, TU Muenchen Equality reasoning based on congurence closure. It features: * congruence closure for any term that participates in equalities * support for predicates These features might be added: * caching of explanations while building proofs to obtain shorter proofs and faster proof checking * propagating relevant merges of equivalence classes to all other theory solvers * propagating new relevant negated equalities to all other theory solvers * creating lemma "f ~= g | a ~= b | f a = g b" for asserted negated equalities between "f a" and "g b" (dynamic ackermannization) The implementation is inspired by: Robert Nieuwenhuis and Albert Oliveras. Fast Congruence Closure and Extensions. In Information and Computation, volume 205(4), pages 557-580, 2007. Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, Cesare Tinelli. DPLL(T): Fast decision procedures. In Lecture Notes in Computer Science, volume 3114, pages 175-188. Springer, 2004. *) signature ARGO_CC = sig (* context *) type context val context: context (* enriching the context *) val add_atom: Argo_Term.term -> context -> Argo_Lit.literal option * context (* main operations *) val assume: Argo_Common.literal -> context -> Argo_Lit.literal Argo_Common.implied * context val check: context -> Argo_Lit.literal Argo_Common.implied * context val explain: Argo_Lit.literal -> context -> (Argo_Cls.clause * context) option val add_level: context -> context val backtrack: context -> context end structure Argo_Cc: ARGO_CC = struct (* tables indexed by pairs of terms *) val term2_ord = prod_ord Argo_Term.term_ord Argo_Term.term_ord structure Argo_Term2tab = Table(type key = Argo_Term.term * Argo_Term.term val ord = term2_ord) (* equality certificates *) (* The solver keeps assumed equalities to produce explanations later on. A flat equality (lp, (t1, t2)) consists of the assumed literal and its proof as well as the terms t1 and t2 that are assumed to be equal. The literal expresses the equality t1 = t2. A congruence equality (t1, t2) is an equality t1 = t2 where both terms are applications (f a) and (g b). A symmetric equality eq is a marker for applying the symmetry rule to eq. *) datatype eq = Flat of Argo_Common.literal * (Argo_Term.term * Argo_Term.term) | Cong of Argo_Term.term * Argo_Term.term | Symm of eq fun dest_eq (Flat (_, tp)) = tp | dest_eq (Cong tp) = tp | dest_eq (Symm eq) = swap (dest_eq eq) fun symm (Symm eq) = eq | symm eq = Symm eq fun negate (Flat ((lit, p), tp)) = Flat ((Argo_Lit.negate lit, p), tp) | negate (Cong tp) = Cong tp | negate (Symm eq) = Symm (negate eq) fun dest_app (Argo_Term.T (_, Argo_Expr.App, [t1, t2])) = (t1, t2) | dest_app _ = raise Fail "bad application" (* context *) (* Each representative keeps track of the yet unimplied atoms in which this any member of this representative's equivalence class occurs. An atom is either a list of equalities between two terms, a list of predicates or a certificate. The certificate denotes that this equivalence class contains already implied predicates, and the literal accompanying the certificate specifies the polarity of these predicates. *) datatype atoms = Eqs of (Argo_Term.term * Argo_Term.term) list | Preds of Argo_Term.term list | Cert of Argo_Common.literal (* Each representative has an associated ritem that contains the members of the equivalence class, the yet unimplied atoms and further information. *) type ritem = { size: int, (* the size of the equivalence class *) class: Argo_Term.term list, (* the equivalence class as a list of distinct terms *) occs: Argo_Term.term list, (* a list of all application terms in which members of the equivalence class occur either as function or as argument *) neqs: (Argo_Term.term * eq) list, (* a list of terms from disjoint equivalence classes, for each term of this list there is a certificate of a negated equality that is required to explain why the equivalence classes are disjoint *) atoms: atoms} (* the atoms of the representative *) type repr = Argo_Term.term Argo_Termtab.table type rdata = ritem Argo_Termtab.table type apps = Argo_Term.term Argo_Term2tab.table type trace = (Argo_Term.term * eq) Argo_Termtab.table type context = { repr: repr, (* a table mapping terms to their representatives *) rdata: rdata, (* a table mapping representatives to their ritems *) apps: apps, (* a table mapping a function and an argument to their application *) trace: trace, (* the proof forest used to trace assumed and implied equalities *) prf: Argo_Proof.context, (* the proof context *) back: (repr * rdata * apps * trace) list} (* backtracking information *) fun mk_context repr rdata apps trace prf back: context = {repr=repr, rdata=rdata, apps=apps, trace=trace, prf=prf, back=back} val context = mk_context Argo_Termtab.empty Argo_Termtab.empty Argo_Term2tab.empty Argo_Termtab.empty Argo_Proof.cc_context [] fun repr_of repr t = the_default t (Argo_Termtab.lookup repr t) fun repr_of' ({repr, ...}: context) = repr_of repr fun put_repr t r = Argo_Termtab.update (t, r) fun mk_ritem size class occs neqs atoms: ritem = {size=size, class=class, occs=occs, neqs=neqs, atoms=atoms} fun as_ritem t = mk_ritem 1 [t] [] [] (Eqs []) fun as_pred_ritem t = mk_ritem 1 [t] [] [] (Preds [t]) fun gen_ritem_of mk rdata r = the_default (mk r) (Argo_Termtab.lookup rdata r) fun ritem_of rdata = gen_ritem_of as_ritem rdata fun ritem_of_pred rdata = gen_ritem_of as_pred_ritem rdata fun ritem_of' ({rdata, ...}: context) = ritem_of rdata fun put_ritem r ri = Argo_Termtab.update (r, ri) fun add_occ r occ = Argo_Termtab.map_default (r, as_ritem r) (fn {size, class, occs, neqs, atoms}: ritem => mk_ritem size class (occ :: occs) neqs atoms) fun put_atoms atoms ({size, class, occs, neqs, ...}: ritem) = mk_ritem size class occs neqs atoms fun add_eq_atom r atom = Argo_Termtab.map_default (r, as_ritem r) (fn ri as {atoms=Eqs atoms, ...}: ritem => put_atoms (Eqs (atom :: atoms)) ri | ri => put_atoms (Eqs [atom]) ri) fun lookup_app apps tp = Argo_Term2tab.lookup apps tp fun put_app tp app = Argo_Term2tab.update_new (tp, app) (* traces for explanations *) (* Assumed and implied equalities are collected in a proof forest for being able to produce explanations. For each equivalence class there is one proof tree. The equality certificates are oriented towards a root term, that is not necessarily the representative of the equivalence class. *) (* Whenever two equivalence classes are merged due to an equality t1 = t2, the shorter of the two paths, either from t1 to its root or t2 to its root, is re-oriented such that the relevant ti becomes the new root of its tree. Then, a new edge between ti and the other term of the equality t1 = t2 is added to connect the two proof trees. *) fun depth_of trace t = (case Argo_Termtab.lookup trace t of NONE => 0 | SOME (t', _) => 1 + depth_of trace t') fun reorient t trace = (case Argo_Termtab.lookup trace t of NONE => trace | SOME (t', eq) => Argo_Termtab.update (t', (t, symm eq)) (reorient t' trace)) fun new_edge from to eq trace = Argo_Termtab.update (from, (to, eq)) (reorient from trace) fun with_shortest f (t1, t2) eq trace = (if depth_of trace t1 <= depth_of trace t2 then f t1 t2 eq else f t2 t1 (symm eq)) trace fun add_edge eq trace = with_shortest new_edge (dest_eq eq) eq trace (* To produce an explanation that t1 and t2 are equal, the paths to their root are extracted from the proof forest. Common ancestors in both paths are dropped. *) fun path_to_root trace path t = (case Argo_Termtab.lookup trace t of NONE => (t, path) | SOME (t', _) => path_to_root trace (t :: path) t') fun drop_common root (t1 :: path1) (t2 :: path2) = if Argo_Term.eq_term (t1, t2) then drop_common t1 path1 path2 else root | drop_common root _ _ = root fun common_ancestor trace t1 t2 = let val ((root, path1), (_, path2)) = apply2 (path_to_root trace []) (t1, t2) in drop_common root path1 path2 end (* The proof of an assumed literal is typically a hypothesis. If the assumed literal is already known to be a unit literal, then there is already a proof for it. *) fun proof_of (lit, NONE) lits prf = (insert Argo_Lit.eq_lit (Argo_Lit.negate lit) lits, Argo_Proof.mk_hyp lit prf) | proof_of (_, SOME p) lits prf = (lits, (p, prf)) (* The explanation of equality between two terms t1 and t2 is computed based on the paths from t1 and t2 to their common ancestor t in the proof forest. For each of the two paths, a transitive proof of equality t1 = t and t = t2 is constructed, such that t1 = t2 follows by transitivity. Each edge of the paths denotes an assumed or implied equality. Implied equalities might be due to congruences (f a = g b) for which the equalities f = g and a = b need to be explained recursively. *) fun mk_eq_proof trace t1 t2 lits prf = if Argo_Term.eq_term (t1, t2) then (lits, Argo_Proof.mk_refl t1 prf) else let val root = common_ancestor trace t1 t2 val (lits, (p1, prf)) = trans_proof I I trace t1 root lits prf val (lits, (p2, prf)) = trans_proof swap symm trace t2 root lits prf in (lits, Argo_Proof.mk_trans p1 p2 prf) end and trans_proof sw sy trace t root lits prf = if Argo_Term.eq_term (t, root) then (lits, Argo_Proof.mk_refl t prf) else (case Argo_Termtab.lookup trace t of NONE => raise Fail "bad trace" | SOME (t', eq) => let val (lits, (p1, prf)) = proof_step trace (sy eq) lits prf val (lits, (p2, prf)) = trans_proof sw sy trace t' root lits prf in (lits, uncurry Argo_Proof.mk_trans (sw (p1, p2)) prf) end) and proof_step _ (Flat (cert, _)) lits prf = proof_of cert lits prf | proof_step trace (Cong tp) lits prf = let val ((t1, t2), (u1, u2)) = apply2 dest_app tp val (lits, (p1, prf)) = mk_eq_proof trace t1 u1 lits prf val (lits, (p2, prf)) = mk_eq_proof trace t2 u2 lits prf in (lits, Argo_Proof.mk_cong p1 p2 prf) end | proof_step trace (Symm eq) lits prf = proof_step trace eq lits prf ||> uncurry Argo_Proof.mk_symm (* All clauses produced by a theory solver are expected to be a lemma. The lemma proof must hence be the last proof step. *) fun close_proof lit lits (p, prf) = (lit :: lits, Argo_Proof.mk_lemma [lit] p prf) (* The explanation for the equality of t1 and t2 used the above algorithm. *) fun explain_eq lit t1 t2 ({repr, rdata, apps, trace, prf, back}: context) = let val (lits, (p, prf)) = mk_eq_proof trace t1 t2 [] prf |-> close_proof lit in ((lits, p), mk_context repr rdata apps trace prf back) end (* The explanation that t1 and t2 are distinct uses the negated equality u1 ~= u2 that explains why the equivalence class containing t1 and u1 and the equivalence class containing t2 and u2 are disjoint. The explanations for t1 = u1 and u2 = t2 are constructed using the above algorithm. By transitivity, it follows that t1 ~= t2. *) fun finish_proof (Flat ((lit, _), _)) lits p prf = close_proof lit lits (p, prf) | finish_proof (Cong _) _ _ _ = raise Fail "bad equality" | finish_proof (Symm eq) lits p prf = Argo_Proof.mk_symm p prf |-> finish_proof eq lits fun explain_neq eq eq' ({repr, rdata, apps, trace, prf, back}: context) = let val (t1, t2) = dest_eq eq val (u1, u2) = dest_eq eq' val (lits, (p, prf)) = proof_step trace eq' [] prf val (lits, (p1, prf)) = mk_eq_proof trace t1 u1 lits prf val (lits, (p2, prf)) = mk_eq_proof trace u2 t2 lits prf val (lits, (p, prf)) = Argo_Proof.mk_trans p p2 prf |-> Argo_Proof.mk_trans p1 |-> finish_proof eq lits in ((lits, p), mk_context repr rdata apps trace prf back) end (* propagating new equalities *) exception CONFLICT of Argo_Cls.clause * context (* comment missing *) fun same_repr repr r (t, _) = Argo_Term.eq_term (r, repr_of repr t) fun has_atom rdata r eq = (case #atoms (ritem_of rdata r) of Eqs eqs => member (Argo_Term.eq_term o snd) eqs eq | _ => false) fun add_implied mk_lit repr rdata r neqs (atom as (t, eq)) (eqs, ls) = let val r' = repr_of repr t in if Argo_Term.eq_term (r, r') then (eqs, insert Argo_Lit.eq_lit (mk_lit eq) ls) else if exists (same_repr repr r') neqs andalso has_atom rdata r' eq then (eqs, Argo_Lit.Neg eq :: ls) else (atom :: eqs, ls) end (* comment missing *) fun copy_occ repr app (eqs, occs, apps) = let val rp = apply2 (repr_of repr) (dest_app app) in (case lookup_app apps rp of SOME app' => (Cong (app, app') :: eqs, occs, apps) | NONE => (eqs, app :: occs, put_app rp app apps)) end (* comment missing *) fun add_lits (Argo_Lit.Pos _, _) = fold (cons o Argo_Lit.Pos) | add_lits (Argo_Lit.Neg _, _) = fold (cons o Argo_Lit.Neg) fun join_atoms f (Eqs eqs1) (Eqs eqs2) ls = f eqs1 eqs2 ls | join_atoms _ (Preds ts1) (Preds ts2) ls = (Preds (union Argo_Term.eq_term ts1 ts2), ls) | join_atoms _ (Preds ts) (Cert lp) ls = (Cert lp, add_lits lp ts ls) | join_atoms _ (Cert lp) (Preds ts) ls = (Cert lp, add_lits lp ts ls) | join_atoms _ (Cert lp) (Cert _) ls = (Cert lp, ls) | join_atoms _ _ _ _ = raise Fail "bad atoms" (* comment missing *) fun join r1 ri1 r2 ri2 eq (eqs, ls, {repr, rdata, apps, trace, prf, back}: context) = let val {size=size1, class=class1, occs=occs1, neqs=neqs1, atoms=atoms1}: ritem = ri1 val {size=size2, class=class2, occs=occs2, neqs=neqs2, atoms=atoms2}: ritem = ri2 val repr = fold (fn t => put_repr t r1) class2 repr val class = fold cons class2 class1 val (eqs, occs, apps) = fold (copy_occ repr) occs2 (eqs, occs1, apps) val trace = add_edge eq trace val neqs = AList.merge Argo_Term.eq_term (K true) (neqs1, neqs2) fun add r neqs = fold (add_implied Argo_Lit.Pos repr rdata r neqs) fun adds eqs1 eqs2 ls = ([], ls) |> add r2 neqs2 eqs1 |> add r1 neqs1 eqs2 |>> Eqs val (atoms, ls) = join_atoms adds atoms1 atoms2 ls (* TODO: make sure that all implied literals are propagated *) val rdata = put_ritem r1 (mk_ritem (size1 + size2) class occs neqs atoms) rdata in (eqs, ls, mk_context repr rdata apps trace prf back) end (* comment missing *) fun find_neq ({repr, ...}: context) ({neqs, ...}: ritem) r = find_first (same_repr repr r) neqs fun check_join (r1, r2) (ri1, ri2) eq (ecx as (_, _, cx)) = (case find_neq cx ri2 r1 of SOME (_, eq') => raise CONFLICT (explain_neq (negate (symm eq)) eq' cx) | NONE => (case find_neq cx ri1 r2 of SOME (_, eq') => raise CONFLICT (explain_neq (negate eq) eq' cx) | NONE => join r1 ri1 r2 ri2 eq ecx)) (* comment missing *) fun with_max_class f (rp as (r1, r2)) (rip as (ri1: ritem, ri2: ritem)) eq = if #size ri1 >= #size ri2 then f rp rip eq else f (r2, r1) (ri2, ri1) (symm eq) (* comment missing *) fun propagate ([], ls, cx) = (rev ls, cx) | propagate (eq :: eqs, ls, cx) = let val rp = apply2 (repr_of' cx) (dest_eq eq) in if Argo_Term.eq_term rp then propagate (eqs, ls, cx) else propagate (with_max_class check_join rp (apply2 (ritem_of' cx) rp) eq (eqs, ls, cx)) end fun without lit (lits, cx) = (Argo_Common.Implied (remove Argo_Lit.eq_lit lit lits), cx) fun flat_merge (lp as (lit, _)) eq cx = without lit (propagate ([Flat (lp, eq)], [], cx)) handle CONFLICT (cls, cx) => (Argo_Common.Conflict cls, cx) (* comment missing *) fun app_merge app tp (cx as {repr, rdata, apps, trace, prf, back}: context) = let val rp as (r1, r2) = apply2 (repr_of repr) tp in (case lookup_app apps rp of SOME app' => (case propagate ([Cong (app, app')], [], cx) of ([], cx) => cx | _ => raise Fail "bad application merge") | NONE => let val rdata = add_occ r1 app (add_occ r2 app rdata) in mk_context repr rdata (put_app rp app apps) trace prf back end) end (* A negated equality between t1 and t2 is only recorded if t1 and t2 are not already known to belong to the same class. In that case, a conflict is raised with an explanation why t1 and t2 are equal. Otherwise, the classes of t1 and t2 are marked as disjoint by storing the negated equality in the ritems of t1's and t2's representative. All equalities between terms of t1's and t2's class are implied as negated equalities. Those equalities are found in the ritems of t1's and t2's representative. *) fun note_neq eq (r1, r2) (t1, t2) ({repr, rdata, apps, trace, prf, back}: context) = let val {size=size1, class=class1, occs=occs1, neqs=neqs1, atoms=atoms1}: ritem = ritem_of rdata r1 val {size=size2, class=class2, occs=occs2, neqs=neqs2, atoms=atoms2}: ritem = ritem_of rdata r2 fun add r (Eqs eqs) ls = fold (add_implied Argo_Lit.Neg repr rdata r []) eqs ([], ls) |>> Eqs | add _ _ _ = raise Fail "bad negated equality between predicates" val ((atoms1, atoms2), ls) = [] |> add r2 atoms1 ||>> add r1 atoms2 val ri1 = mk_ritem size1 class1 occs1 ((t2, eq) :: neqs1) atoms1 val ri2 = mk_ritem size2 class2 occs2 ((t1, symm eq) :: neqs2) atoms2 in (ls, mk_context repr (put_ritem r1 ri1 (put_ritem r2 ri2 rdata)) apps trace prf back) end fun flat_neq (lp as (lit, _)) (tp as (t1, t2)) cx = let val rp = apply2 (repr_of' cx) tp in if Argo_Term.eq_term rp then let val (cls, cx) = explain_eq (Argo_Lit.negate lit) t1 t2 cx in (Argo_Common.Conflict cls, cx) end else without lit (note_neq (Flat (lp, tp)) rp tp cx) end (* declaring atoms *) (* Only a genuinely new equality term t for the equality "t1 = t2" is added. If t1 and t2 belong to the same equality class or if the classes of t1 and t2 are known to be disjoint, the respective literal is returned together with an unmodified context. *) fun add_eq_term t t1 t2 (rp as (r1, r2)) (cx as {repr, rdata, apps, trace, prf, back}: context) = if Argo_Term.eq_term rp then (SOME (Argo_Lit.Pos t), cx) else if is_some (find_neq cx (ritem_of rdata r1) r2) then (SOME (Argo_Lit.Neg t), cx) else let val rdata = add_eq_atom r1 (t2, t) (add_eq_atom r2 (t1, t) rdata) in (NONE, mk_context repr rdata apps trace prf back) end (* Only a genuinely new predicate t, which is an application "t1 t2", is added. If there is a predicate that is known to be congruent to the representatives of t1 and t2, and that predicate or its negation has already been assummed, the respective literal of t is returned together with an unmodified context. *) fun add_pred_term t rp (cx as {repr, rdata, apps, trace, prf, back}: context) = (case lookup_app apps rp of NONE => (NONE, mk_context repr (put_ritem t (as_pred_ritem t) rdata) apps trace prf back) | SOME app => (case `(ritem_of_pred rdata) (repr_of repr app) of ({atoms=Cert (Argo_Lit.Pos _, _), ...}: ritem, _) => (SOME (Argo_Lit.Pos t), cx) | ({atoms=Cert (Argo_Lit.Neg _, _), ...}: ritem, _) => (SOME (Argo_Lit.Neg t), cx) | (ri as {atoms=Preds ts, ...}: ritem, r) => let val rdata = put_ritem r (put_atoms (Preds (t :: ts)) ri) rdata in (NONE, mk_context repr rdata apps trace prf back) end | ({atoms=Eqs _, ...}: ritem, _) => raise Fail "bad predicate")) (* For each term t that is an application "t1 t2", the reflexive equality t = t1 t2 is added to the context. This is required for propagations of congruences. *) fun flatten (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])) cx = flatten t1 (flatten t2 (app_merge t (t1, t2) cx)) | flatten _ cx = cx (* Atoms to be added to the context must either be an equality "t1 = t2" or an application "t1 t2" (a predicate). Besides adding the equality or the application, reflexive equalities for for all applications in the terms t1 and t2 are added. *) fun add_atom (t as Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])) cx = add_eq_term t t1 t2 (apply2 (repr_of' cx) (t1, t2)) (flatten t1 (flatten t2 cx)) | add_atom (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])) cx = let val cx = flatten t1 (flatten t2 (app_merge t (t1, t2) cx)) in add_pred_term t (apply2 (repr_of' cx) (t1, t2)) cx end | add_atom _ cx = (NONE, cx) (* assuming external knowledge *) (* Assuming a predicate r replaces all predicate atoms of r's ritem with the assumed certificate. The predicate atoms are implied, either with positive or with negative polarity based on the assumption. There must not be a certificate for r since otherwise r would have been assumed before already. *) fun assume_pred lit mk_lit cert r ({repr, rdata, apps, trace, prf, back}: context) = (case ritem_of_pred rdata r of {size, class, occs, neqs, atoms=Preds ts}: ritem => let val rdata = put_ritem r (mk_ritem size class occs neqs cert) rdata in without lit (map mk_lit ts, mk_context repr rdata apps trace prf back) end | _ => raise Fail "bad predicate assumption") (* Assumed equalities "t1 = t2" are treated as flat equalities between terms t1 and t2. If t1 and t2 are applications, congruences are propagated as part of the merge between t1 and t2. Negated equalities are handled likewise. Assumed predicates do not trigger congruences. Only predicates of the same class are implied. *) fun assume (lp as (Argo_Lit.Pos (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])), _)) cx = flat_merge lp (t1, t2) cx | assume (lp as (Argo_Lit.Neg (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2])), _)) cx = flat_neq lp (t1, t2) cx | assume (lp as (lit as Argo_Lit.Pos (t as Argo_Term.T (_, Argo_Expr.App, [_, _])), _)) cx = assume_pred lit Argo_Lit.Pos (Cert lp) (repr_of' cx t) cx | assume (lp as (lit as Argo_Lit.Neg (t as Argo_Term.T (_, Argo_Expr.App, [_, _])), _)) cx = assume_pred lit Argo_Lit.Neg (Cert lp) (repr_of' cx t) cx | assume _ cx = (Argo_Common.Implied [], cx) (* checking for consistency and pending implications *) (* The internal model is always kept consistent. All implications are propagated as soon as new information is assumed. Hence, there is nothing to be done here. *) fun check cx = (Argo_Common.Implied [], cx) (* explanations *) (* The explanation for the predicate t, which is an application of t1 and t2, is constructed from the explanation of the predicate application "u1 u2" as well as the equalities "u1 = t1" and "u2 = t2" which both are constructed from the proof forest. The substitution rule is the proof step that concludes "t1 t2" from "u1 u2" and the two equalities "u1 = t1" and "u2 = t2". The atoms part of the ritem of t's representative must be a certificate of an already assumed predicate for otherwise there would be no explanation for t. *) fun explain_pred lit t t1 t2 ({repr, rdata, apps, trace, prf, back}: context) = (case ritem_of_pred rdata (repr_of repr t) of {atoms=Cert (cert as (lit', _)), ...}: ritem => let val (u1, u2) = dest_app (Argo_Lit.term_of lit') val (lits, (p, prf)) = proof_of cert [] prf val (lits, (p1, prf)) = mk_eq_proof trace u1 t1 lits prf val (lits, (p2, prf)) = mk_eq_proof trace u2 t2 lits prf val (lits, (p, prf)) = Argo_Proof.mk_subst p p1 p2 prf |> close_proof lit lits in ((lits, p), mk_context repr rdata apps trace prf back) end | _ => raise Fail "no explanation for bad predicate") (* Explanations are produced based on the proof forest that is constructed while assuming new information and propagating this among the internal data structures. For predicates, no distinction between both polarities needs to be done here. The atoms part of the relevant ritem knows the assumed polarity. *) fun explain (lit as Argo_Lit.Pos (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2]))) cx = SOME (explain_eq lit t1 t2 cx) | explain (lit as Argo_Lit.Neg (Argo_Term.T (_, Argo_Expr.Eq, [t1, t2]))) cx = let val (_, eq) = the (find_neq cx (ritem_of' cx (repr_of' cx t1)) (repr_of' cx t2)) in SOME (explain_neq (Flat ((lit, NONE), (t1, t2))) eq cx) end | explain (lit as (Argo_Lit.Pos (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])))) cx = SOME (explain_pred lit t t1 t2 cx) | explain (lit as (Argo_Lit.Neg (t as Argo_Term.T (_, Argo_Expr.App, [t1, t2])))) cx = SOME (explain_pred lit t t1 t2 cx) | explain _ _ = NONE (* backtracking *) (* All information that needs to be reconstructed on backtracking is stored on the backtracking stack. On backtracking any current information is replaced by what was stored before. No copying nor subtle updates are required thanks to immutable data structures. *) fun add_level ({repr, rdata, apps, trace, prf, back}: context) = mk_context repr rdata apps trace prf ((repr, rdata, apps, trace) :: back) fun backtrack ({back=[], ...}: context) = raise Empty | backtrack ({prf, back=(repr, rdata, apps, trace) :: back, ...}: context) = mk_context repr rdata apps trace prf back end