Support Sort.getInstantiatedParameters.

Author: abdoo8080

cvc5.lean

@@ -619,6 +619,12 @@ extern_def!? getNullableElementSort : cvc5.Sort → Except Error cvc5.Sort
 /-- Get the associated uninterpreted sort constructor of an instantiated uninterpreted sort. -/
 extern_def!? getUninterpretedSortConstructor : cvc5.Sort → Except Error cvc5.Sort
 
+/-- Get the sorts used to instantiate the sort parameters of a parametric sort.
+
+A parametric sort is a parametric datatype or an uninterpreted sort constructor sort.
+See `cvc5.Sort.instantiate`. -/
+extern_def!? getInstantiatedParameters : cvc5.Sort → Except Error (Array cvc5.Sort)
+
 /-- Instantiate a parameterized datatype sort or uninterpreted sort constructor sort.
 
 Create sort parameters with `TermManager.mkParamSort symbol`.

ffi/ffi.cpp

@@ -686,6 +686,19 @@ LEAN_EXPORT lean_obj_res sort_getUninterpretedSortConstructor(lean_obj_arg s)
   CVC5_LEAN_API_TRY_CATCH_EXCEPT_END;
 }
 
+LEAN_EXPORT lean_obj_res sort_getInstantiatedParameters(lean_obj_arg s)
+{
+  CVC5_LEAN_API_TRY_CATCH_EXCEPT_BEGIN;
+  std::vector<Sort> params = sort_unbox(s)->getInstantiatedParameters();
+  lean_object* ps = lean_mk_empty_array();
+  for (const Sort& param : params)
+  {
+    ps = lean_array_push(ps, sort_box(new Sort(param)));
+  }
+  return except_ok(lean_box(0), ps);
+  CVC5_LEAN_API_TRY_CATCH_EXCEPT_END;
+}
+
 LEAN_EXPORT lean_obj_arg sort_instantiate(lean_obj_arg s, lean_obj_arg params)
 {
   CVC5_LEAN_API_TRY_CATCH_EXCEPT_BEGIN;