-- \BusinessProcess

module GUI.Vers1.BusinessProcess where

open import Data.String
open import Data.List renaming (map to mapL)
open import Data.Product hiding (map)
open import Data.Nat
open import Size
open import Data.Fin renaming (_+_ to _+fin_)

open import heap.libraryVec
open import GUI.Vers1.GUIDefinitions
open import GUI.Vers1.GUIDefinitionsBase
open import GUI.Vers1.GUIExampleLib
open import StateSizedIO.GUI.BaseStateDependent

  -- \BusinessProcess
data BusinessProcess : Set where
  startEvent :  String  BusinessProcess  BusinessProcess
  endEvent  :  String  BusinessProcess
  xor        :  List (String ×  BusinessProcess)
  input      :  {n : }  Tuple String n
                  (Tuple String n  BusinessProcess)
  activity     :  String  BusinessProcess  BusinessProcess

-- with Tuple slit m into (str' , m)
--  and used str' for the first two and m for the last goal

  businessModel2GUI :  {i}   BusinessProcess
                              GUI {i}
  businessModel2GUI (endEvent x) = endEventGUI x
  businessModel2GUI (xor l) = businessModel2GUIxor l
  businessModel2GUI (input {n} str f) = multiTextboxGUI n str  v  businessModel2GUI (f v))
  businessModel2GUI (activity str b)  =   onebuttonStrGUI str (businessModel2GUI b)
  businessModel2GUI (startEvent str b)  =   onebuttonStrGUI str (businessModel2GUI b)

-- an unsized version for presentation purposes
-- \BusinessProcess
  businessModel2Gui : BusinessProcess  GUI
  businessModel2Gui = businessModel2GUI {}

  businessModel2GUIxor : {i : Size}  List (String × BusinessProcess)  GUI {i}
  businessModel2GUIxor [] .gui = emptyFrame
  businessModel2GUIxor [] .obj .method ()
  businessModel2GUIxor ((str , _)  l) .gui = addButton str (businessModel2GUIxor l .gui)
  businessModel2GUIxor ((str , g)  l) .obj .method (zero , _) = returnGUI  (businessModel2GUI g)
  businessModel2GUIxor ((str , _)  l) .obj .method (suc m , s) = businessModel2GUIxor l .obj .method (m , s)