* Add helper functions to load REAL libraries and set theorem to evaluate

src/python/ocarina-python_cmd.adb

@@ -193,6 +193,44 @@ package body Ocarina.Python_Cmd is
       Set_Return_Value (Data, Result);
    end On_Instantiate;
 
+   -------------------------
+   -- On_Set_REAL_Theorem --
+   -------------------------
+
+   procedure On_Set_REAL_Theorem
+     (Data : in out Callback_Data'Class; Command : String);
+
+   procedure On_Set_REAL_Theorem
+     (Data : in out Callback_Data'Class;
+      Command : String)
+   is
+      pragma Unreferenced (Command);
+      Result : constant Boolean :=
+        Ocarina.Utils.Set_REAL_Theorem (Nth_Arg (Data, 1, ""));
+
+   begin
+      Set_Return_Value (Data, Result);
+   end On_Set_REAL_Theorem;
+
+   -------------------------
+   -- On_Add_REAL_Library --
+   -------------------------
+
+   procedure On_Add_REAL_Library
+     (Data : in out Callback_Data'Class; Command : String);
+
+   procedure On_Add_REAL_Library
+     (Data : in out Callback_Data'Class;
+      Command : String)
+   is
+      pragma Unreferenced (Command);
+      Result : constant Boolean :=
+        Ocarina.Utils.Add_REAL_Library (Nth_Arg (Data, 1, ""));
+
+   begin
+      Set_Return_Value (Data, Result);
+   end On_Add_REAL_Library;
+
    ----------------------
    -- On_Get_AADL_Root --
    ----------------------
@@ -761,6 +799,16 @@ package body Ocarina.Python_Cmd is
         (Repo, "instantiate", 1, 1,
          Handler => On_Instantiate'Unrestricted_Access);
 
+      --  set_real_theorem() function
+      Register_Command
+        (Repo, "set_real_theorem", 1, 1,
+         Handler => On_Set_REAL_Theorem'Unrestricted_Access);
+
+      --  add_real_library() function
+      Register_Command
+        (Repo, "add_real_library", 1, 1,
+         Handler => On_Add_REAL_Library'Unrestricted_Access);
+
       --  getRoot() function
       Register_Command
         (Repo, "getRoot", 0, 0,
@@ -791,12 +839,15 @@ package body Ocarina.Python_Cmd is
         (Repo, "getNodeId", 1, 1,
          Handler => On_Get_Node_Id'Unrestricted_Access);
 
-      Repo := Ocarina.ME_AADL.AADL_Instances.Nodes.Python.
-         Register_Generated_Functions (Repo);
+      --  Register functions generated from AADL declarative and
+      --  instance trees
 
       Repo := Ocarina.ME_AADL.AADL_Tree.Nodes.Python.
          Register_Generated_Functions (Repo);
 
+      Repo := Ocarina.ME_AADL.AADL_Instances.Nodes.Python.
+         Register_Generated_Functions (Repo);
+
       return Repo;
    end Register_Scripts_And_Functions;
 

src/python/ocarina-utils.adb

@@ -36,10 +36,12 @@ with Ocarina.Output;             use Ocarina.Output;
 with Utils;                      use Utils;
 
 with Ocarina.Analyzer;           use Ocarina.Analyzer;
+with Ocarina.Analyzer.REAL;      use Ocarina.Analyzer.REAL;
 with Ocarina.Backends;           use Ocarina.Backends;
 with Ocarina.Configuration;      use Ocarina.Configuration;
 with Ocarina.FE_AADL;            use Ocarina.FE_AADL;
 with Ocarina.FE_AADL.Parser;
+with Ocarina.FE_REAL.Parser;     use Ocarina.FE_REAL.Parser;
 with Ocarina.Instances;          use Ocarina.Instances;
 with Ocarina.Parser;             use Ocarina.Parser;
 with Ocarina.Options;            use Ocarina.Options;
@@ -136,6 +138,33 @@ package body Ocarina.Utils is
       return Success;
    end Analyze;
 
+   ----------------------
+   -- Set_REAL_Theorem --
+   ----------------------
+
+   function Set_REAL_Theorem (Theorem_Name : String) return Boolean is
+   begin
+      if Theorem_Name /= "" then
+         Write_Line ("Been there");
+         Main_Theorem := To_Lower (Get_String_Name (Theorem_Name));
+      end if;
+
+      return True;
+   end Set_REAL_Theorem;
+
+   ----------------------
+   -- Add_REAL_Library --
+   ----------------------
+
+   function Add_REAL_Library (Library_Name : String) return Boolean is
+   begin
+      if Library_Name /= "" then
+         Write_Line ("Adding: " & Library_Name);
+         Load_REAL_Library (Get_String_Name (Library_Name));
+      end if;
+      return True;
+   end Add_REAL_Library;
+
    -----------------
    -- Instantiate --
    -----------------

src/python/ocarina-utils.ads

@@ -41,6 +41,8 @@ package Ocarina.Utils is
    function Instantiate (Root_System : String) return Boolean;
    procedure Generate (Backend_Name : String);
    procedure Reset;
+   function Set_REAL_Theorem (Theorem_Name : String) return Boolean;
+   function Add_REAL_Library (Library_Name : String) return Boolean;
 
    function Get_AADL_Root return Node_Id;
    function Get_Node_Id_From_String (Name : String) return Node_Id;