Klean: implement ^%Int and rename generated abs to kabs (#4836)

This PR implements the `^%Int` function and renames the generated `abs`
function to `kabs` to not collide with Mathlib's `abs` function.

Author: JuanCoRo

pyk/src/pyk/klean/k2lean4.py

@@ -67,6 +67,7 @@
     "Lbl'UndsStar'Int'Unds'",  # *Int
     "Lbl'UndsSlsh'Int'Unds'",  # /Int
     "Lbl'Unds'modInt'Unds'",  # modInt
+    "Lbl'UndsXor-Perc'Int'UndsUnds'",  # ^%Int
     "LblmaxInt'LParUndsCommUndsRParUnds'INT-COMMON'Unds'Int'Unds'Int'Unds'Int",  # maxInt
     "Lbl'Tild'Int'Unds'",  # ~Int
     "Lbl'Unds-LT-Eqls'Int'Unds'",  # <=Int
@@ -87,6 +88,7 @@
 
 _SYMBOL_OVERRIDES: Final = {
     'Lblite': 'kite',
+    'Lblabs': 'kabs',
 }
 
 

pyk/src/pyk/klean/template/{{ cookiecutter.package_name }}/{{ cookiecutter.library_name }}/Prelude.lean

@@ -241,8 +241,13 @@ def «_-Int_» (x0 x1 : SortInt) : Option SortInt := some (x0 - x1)
 def «_*Int_» (x0 x1 : SortInt) : Option SortInt := some (x0 * x1)
 def «_/Int_» (x0 x1 : SortInt) : Option SortInt :=
   ite (x1 == 0) none (Int.tdiv x0 x1)
-def _modInt_ (x0 : SortInt) (x1 : SortInt) : Option SortInt :=
+def _modInt_ (x0 x1 : SortInt) : Option SortInt :=
   ite (x1 == 0) none (Int.emod x0 x1)
+def «_^%Int__» (x0 x1 x2 : SortInt) : Option SortInt :=
+   if x2 == 0 then none else
+   match x1 with -- TODO: Revisit this implementation
+   | .ofNat n => some (Int.emod (Int.pow x0 n) x2)
+   | _ => none
 def «maxInt(_,_)_INT-COMMON_Int_Int_Int» (x0 x1 : SortInt) :=
   some (ite (x0 < x1) x1 x0)
 def «log2Int(_)_INT-COMMON_Int_Int» (x0 : SortInt) : Option SortInt :=