search

OCamlPro / alt-ergo

OCamlPro public development repository for Alt-Ergo
https://alt-ergo.ocamlpro.com/
Other
130 stars 33 forks source link

Refactoring `Adt_rel` using domains on class representatives only #1087

Closed Halbaroth closed 4 months ago

Halbaroth commented 5 months ago

This PR is rebased on #1078 and #1086.

Halbaroth commented 4 months ago

As explained offline, we cannot use X.extract_term as we was done in casesplit in a previous version of this PR because there is no implementation of term_extract for AC symbols. For instance the following input file:

type t = A | B of { d : int }
logic e1, e2 : t
logic ac u : t, t -> t 

axiom a1 : e1 <> e2
axiom a2 : (u(e1, e2) ? B)
goal g : (u(e2, e1) ? B)

raises an exception with Alt-Ergo v2.5.3 for the same reason because we used X.term_extract in deduce_is_constr.

In the new implementation of casesplit, we produces a semantic literal instead of a syntactical one.

Halbaroth commented 4 months ago

@bclement-ocp ping