Minor fixes.

Author: abdoo8080

cvc5.lean

@@ -1144,7 +1144,7 @@ namespace EnvT
 /-- Runs `EnvT` code. -/
 def run [Monad m] [MonadLiftT BaseIO m] (code : EnvT m α) : m (Except Error α) := code
 
-example [Monad m] [MonadLiftT BaseIO m] : MonadLift Env (EnvT m) where
+instance [Monad m] [MonadLiftT BaseIO m] : MonadLift Env (EnvT m) where
   monadLift code := do
     match ← liftM <| run code with
     | .ok a => return a
@@ -1328,7 +1328,7 @@ extern_def proofToString : (solver : Solver) → Proof → Env String
 Commands that produce a result such as `(check-sat)`, `(get-model)`, ... are executed but the
 results are ignored.
 -/
-extern_def parseCommands : (solver : Solver) → (query : String) → Env String
+extern_def parseCommands : (solver : Solver) → (query : String) → Env (Array cvc5.Sort × Array Term)
 
 end Solver
 

ffi/ffi.cpp

@@ -1746,7 +1746,19 @@ LEAN_EXPORT lean_obj_res solver_parseCommands(lean_obj_arg solver,
     // to out
     cmd.invoke(slv, sm, out);
   }
-  return env_val(mk_unit_unit(), ioWorld);
+  std::vector<Sort> sortVars = sm->getDeclaredSorts();
+  lean_object* svs = lean_mk_empty_array();
+  for (const Sort& sortVar : sortVars)
+  {
+    svs = lean_array_push(svs, sort_box(new Sort(sortVar)));
+  }
+  std::vector<Term> termVars = sm->getDeclaredTerms();
+  lean_object* tvs = lean_mk_empty_array();
+  for (const Term& termVar : termVars)
+  {
+    tvs = lean_array_push(tvs, term_box(new Term(termVar)));
+  }
+  return env_val(prod_mk(lean_box(0), lean_box(0), svs, tvs), ioWorld);
   CVC5_LEAN_API_TRY_CATCH_ENV_END(ioWorld);
 }
 }

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:4.24.0
+leanprover/lean4:v4.24.0