From d4cbfe9086ad455e01e82dee8df4fd2b5857f547 Mon Sep 17 00:00:00 2001
From: Andrei <16517508+anvacaru@users.noreply.github.com>
Date: Tue, 25 Jun 2024 13:38:15 +0300
Subject: [PATCH] kint.py: add docstrings

---
 pyk/src/pyk/prelude/kint.py                  | 235 ++++++++++++++++++-
 pyk/src/tests/profiling/test-data/domains.md |   6 +-
 2 files changed, 232 insertions(+), 9 deletions(-)

diff --git a/pyk/src/pyk/prelude/kint.py b/pyk/src/pyk/prelude/kint.py
index 8b6c1fda2cc..ab487772617 100644
--- a/pyk/src/pyk/prelude/kint.py
+++ b/pyk/src/pyk/prelude/kint.py
@@ -13,100 +13,323 @@
 
 
 def intToken(i: int) -> KToken:  # noqa: N802
+    r"""Instantiate the KAST term ```#token`(i, "Int")``.
+
+    Args:
+        i: The left operand.
+
+    Returns:
+        The KAST term ```#token`(i, "Int")``.
+    """
     return KToken(str(i), INT)
 
 
 def ltInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_<Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_<Int_`(i1, i2)``.
+    """
     return KApply('_<Int_', i1, i2)
 
 
 def leInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_<=Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_<=Int_`(i1, i2)``.
+    """
     return KApply('_<=Int_', i1, i2)
 
 
 def gtInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_>Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_>Int_`(i1, i2)``.
+    """
     return KApply('_>Int_', i1, i2)
 
 
 def geInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_>=Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_>=Int_`(i1, i2)``.
+    """
     return KApply('_>=Int_', i1, i2)
 
 
 def eqInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_==Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_==Int_`(i1, i2)``.
+    """
     return KApply('_==Int_', i1, i2)
 
 
 def neqInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_=/=Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_=/=Int_`(i1, i2)``.
+    """
     return KApply('_=/=Int_', i1, i2)
 
 
-def notInt(i1: KInner) -> KApply:  # noqa: N802
-    return KApply('~Int_', i1)
+def notInt(i: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```~Int_`(i)``.
+
+    Args:
+        i: The integer operand.
+
+    Returns:
+        The KAST term ```Int_`(i)``.
+    """
+    return KApply('~Int_', i)
 
 
 def expInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_^Int_`(i1, i2)``.
+
+    Args:
+        i1: The base operand.
+        i2: The exponent operand.
+
+    Returns:
+        The KAST term ```_^Int_`(i1, i2)``.
+    """
     return KApply('_^Int_', i1, i2)
 
 
 def expModInt(i1: KInner, i2: KInner, i3: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_^%Int__`(i1, i2, i3)``.
+
+    Args:
+        i1: The dividend operand.
+        i2: The divisior operand.
+        i3: The modulo divisor operand.
+
+    Returns:
+        The KAST term ```_^%Int__`(i1, i2, i3)``.
+    """
     return KApply('_^%Int__', i1, i2, i3)
 
 
 def mulInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_*Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_*Int_`(i1, i2)``.
+    """
     return KApply('_*Int_', i1, i2)
 
 
 def divInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_/Int_`(i1, i2)``.
+
+    Args:
+        i1: The dividend operand.
+        i2: The divisor operand.
+
+    Returns:
+        The KAST term ```_/Int_`(i1, i2)``.
+    """
     return KApply('_/Int_', i1, i2)
 
 
 def modInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_%Int_`(i1, i2)``.
+
+    Args:
+        i1: The dividend operand.
+        i2: The divisor operand.
+
+    Returns:
+        The KAST term ```_%Int_`(i1, i2)``.
+    """
     return KApply('_%Int_', i1, i2)
 
 
 def euclidDivInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_divInt_`(i1, i2)``.
+
+    Args:
+        i1: The dividend operand.
+        i2: The divisor operand.
+
+    Returns:
+        The KAST term ```_divInt_`(i1, i2)``.
+    """
     return KApply('_divInt_', i1, i2)
 
 
 def euclidModInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_modInt_`(i1, i2)``.
+
+    Args:
+        i1: The dividend operand.
+        i2: The divisor operand.
+
+    Returns:
+        The KAST term ```_modInt_`(i1, i2)``.
+    """
     return KApply('_modInt_', i1, i2)
 
 
 def addInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_+Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_+Int_`(i1, i2)``.
+    """
     return KApply('_+Int_', i1, i2)
 
 
 def subInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_-Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_-Int_`(i1, i2)``.
+    """
     return KApply('_-Int_', i1, i2)
 
 
 def rshiftInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_>>Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_>>Int_`(i1, i2)``.
+    """
     return KApply('_>>Int_', i1, i2)
 
 
 def lshiftInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_<<Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_<<Int_`(i1, i2)``.
+    """
     return KApply('_<<Int_', i1, i2)
 
 
 def andInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_&Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_&Int_`(i1, i2)``.
+    """
     return KApply('_&Int_', i1, i2)
 
 
 def xorInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_xorInt_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_xorInt_`(i1, i2)``.
+    """
     return KApply('_xorInt_', i1, i2)
 
 
 def orInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```_|Int_`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```_|Int_`(i1, i2)``.
+    """
     return KApply('_|Int_', i1, i2)
 
 
 def minInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
-    return KApply('minInt(_,_)_INT-COMMON_Int_Int_Int', i1, i2)
+    r"""Instantiate the KAST term ```minInt`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```minInt`(i1, i2)``.
+    """
+    return KApply('minInt', i1, i2)
 
 
 def maxInt(i1: KInner, i2: KInner) -> KApply:  # noqa: N802
-    return KApply('maxInt(_,_)_INT-COMMON_Int_Int_Int', i1, i2)
+    r"""Instantiate the KAST term ```maxInt`(i1, i2)``.
+
+    Args:
+        i1: The left operand.
+        i2: The right operand.
+
+    Returns:
+        The KAST term ```maxInt`(i1, i2)``.
+    """
+    return KApply('maxInt', i1, i2)
+
+
+def absInt(i: KInner) -> KApply:  # noqa: N802
+    r"""Instantiate the KAST term ```absInt`(i)``.
 
+    Args:
+        i: The integer operand.
 
-def absInt(i1: KInner) -> KApply:  # noqa: N802
-    return KApply('absInt(_)_INT-COMMON_Int_Int', i1)
+    Returns:
+        The KAST term ```absInt`(i)``.
+    """
+    return KApply('absInt', i)
diff --git a/pyk/src/tests/profiling/test-data/domains.md b/pyk/src/tests/profiling/test-data/domains.md
index 1f42f186f28..be0803144fb 100644
--- a/pyk/src/tests/profiling/test-data/domains.md
+++ b/pyk/src/tests/profiling/test-data/domains.md
@@ -1257,8 +1257,8 @@ You can:
 You can compute the minimum and maximum `minInt` and `maxInt` of two integers.
 
 ```k
-  syntax Int ::= "minInt" "(" Int "," Int ")"   [function, total, smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)]
-               | "maxInt" "(" Int "," Int ")"   [function, total, smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)]
+  syntax Int ::= "minInt" "(" Int "," Int ")"   [function, total, symbol(minInt), smt-hook((ite (< #1 #2) #1 #2)), hook(INT.min)]
+               | "maxInt" "(" Int "," Int ")"   [function, total, symbol(maxInt), smt-hook((ite (< #1 #2) #2 #1)), hook(INT.max)]
 ```
 
 ### Absolute value
@@ -1266,7 +1266,7 @@ You can compute the minimum and maximum `minInt` and `maxInt` of two integers.
 You can compute the absolute value `absInt` of an integer.
 
 ```k
-  syntax Int ::= absInt ( Int )                 [function, total, smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)]
+  syntax Int ::= absInt ( Int )                 [function, total, symbol(absInt), smt-hook((ite (< #1 0) (- 0 #1) #1)), hook(INT.abs)]
 ```
 
 ### Log base 2