Skip to content

Preds are just Core preds with ✨flavour✨#382

Merged
NatKarmios merged 1 commit into
masterfrom
predicates-as-core
Jul 1, 2026
Merged

Preds are just Core preds with ✨flavour✨#382
NatKarmios merged 1 commit into
masterfrom
predicates-as-core

Conversation

@giltho

@giltho giltho commented Jun 29, 2026

Copy link
Copy Markdown
Contributor

Based on #380, look only at the last commit if you're reviewing this before we merge the others.

The core of this PR is this diff:

	type atom = TypeDef__.assertion_atom =
	  | Emp  (** Empty heap *)
-	  | Pred of string * Expr.t list * Expr.t list  (** Predicates *)
      | Pure of Expr.t  (** Pure formula *)
	  | Types of (Expr.t * Type.t) list  (** Typing assertion *)
	  | CorePred of string * Expr.t list * Expr.t list  (** Core assertion *)
	  | Wand of { lhs : string * Expr.t list; rhs : string * Expr.t list }
	      (** Magic wand of the form [P(...) -* Q(...)] *)

Instead, predicates are now represented as core predicates that start with a magic string GILLIAN_USER_PRED__pred_name.
This does not change the instantiations of Gillian (except for compiling user-defined predicates which do that compilation correctly). Similarly, the GIL parser still parses and produces the old version of the code.

@NatKarmios
NatKarmios force-pushed the predicates-as-core branch from 075d441 to 5d8aae9 Compare July 1, 2026 12:05
@NatKarmios
NatKarmios merged commit 7887daf into master Jul 1, 2026
9 checks passed
@NatKarmios
NatKarmios deleted the predicates-as-core branch July 1, 2026 12:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants