From 7a5c9521182588adf00702daa28bfb11ebf0a37e Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Wed, 12 Aug 2026 15:10:37 -0500
Subject: [PATCH] Construct DatatypeRef and DatatypeSortRef for datatypes

Neither _to_expr_ref nor _to_sort_ref had a datatype case, so a term of a
datatype sort came back as a plain ExprRef and its sort as a plain
SortRef. Const('l', List) was therefore missing the DatatypeRef methods,
and the sort was missing num_constructors(), constructor(), recognizer()
and accessor() - even though Datatype.create() returns a proper
DatatypeSortRef.

Add the missing branch to each. Tuple sorts are datatypes as well, so
TupleSort terms and sorts are now properly wrapped too.

DatatypeRef.sort() no longer needs to build the sort itself and delegates
to _sort.

Fixes the first half of #100.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
---
 cvc5_pythonic_api/cvc5_pythonic.py | 35 +++++++++++++++++++++++++++---
 1 file changed, 32 insertions(+), 3 deletions(-)

diff --git a/cvc5_pythonic_api/cvc5_pythonic.py b/cvc5_pythonic_api/cvc5_pythonic.py
index 6b411cf..3b18d6d 100644
--- a/cvc5_pythonic_api/cvc5_pythonic.py
+++ b/cvc5_pythonic_api/cvc5_pythonic.py
@@ -795,6 +795,8 @@ def _to_sort_ref(s, ctx):
         return FPRMSortRef(s, ctx)
     elif s.isFunction():
         return FuncSortRef(s, ctx)
+    elif s.isDatatype():
+        return DatatypeSortRef(s, ctx)
     return SortRef(s, ctx)
 
 
@@ -1088,6 +1090,8 @@ def _to_expr_ref(a, ctx, r=None):
         return SeqRef(ast, ctx, r)
     if sort.isFunction():
         return FuncDeclRef(ast, ctx, r)
+    if sort.isDatatype():
+        return DatatypeRef(ast, ctx, r)
     return ExprRef(ast, ctx, r)
 
 
@@ -9054,11 +9058,36 @@ def __call__(self, *args):
 
 
 class DatatypeRef(ExprRef):
-    """Datatype expressions."""
+    """Datatype expressions.
+
+    Constants and applications of a datatype sort are instances of this class.
+
+    >>> List = Datatype('List')
+    >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
+    >>> List.declare('nil')
+    >>> List = List.create()
+    >>> isinstance(Const('l', List), DatatypeRef)
+    True
+    >>> isinstance(List.cons(10, List.nil), DatatypeRef)
+    True
+    """
 
     def sort(self):
-        """Return the datatype sort of the datatype expression `self`."""
-        return DatatypeSortRef(self.as_ast().getSort(), self.ctx)
+        """Return the datatype sort of the datatype expression `self`.
+
+        >>> List = Datatype('List')
+        >>> List.declare('cons', ('car', IntSort()), ('cdr', List))
+        >>> List.declare('nil')
+        >>> List = List.create()
+        >>> l = Const('l', List)
+        >>> l.sort()
+        List
+        >>> l.sort().num_constructors()
+        2
+        >>> l.sort().accessor(0, 0)
+        car
+        """
+        return _sort(self.ctx, self.ast)
 
 
 def TupleSort(name, sorts, ctx=None):