content: {-| transpiler to Uppaal, work in progress. -}
  {-# LANGUAGE BlockArguments #-}
  {-# LANGUAGE QuasiQuotes #-}
  {-# LANGUAGE RecordWildCards #-}
  
  module LS.XPile.Uppaal
    ( taSysToString,
      toL4TA
    )
  where
  
  -- import L4.Annotation
  
  import AnyAll qualified as AA
  -- import qualified Data.ByteString.Char8 as T
  import Control.Monad (void)
  import Data.HashSet qualified as Set
  import Data.Maybe (fromMaybe)
  import Data.String.Interpolate (i)
  import Data.Text (unpack)
  import Data.Text qualified as TL
  import L4.PrintProg
    ( PrintConfig (PrintSystem),
      PrintSystem (UppaalStyle),
      ShowL4 (showL4),
    )
  import L4.Syntax as CoreL4
  import L4.SyntaxManipulation
    ( conjsExpr,
      disjsExpr,
      fv,
      mkVarE,
      notExpr,
    )
  import LS.Rule as SFL4R
    ( Rule (Regulative, RuleAlias, cond, hence, rlabel, temporal, upon),
      RuleLabel,
    )
  import LS.Types as SFL4
    ( BoolStructP,
      BoolStructR,
      ParamText,
      RelationalPredicate,
      TComparison (TAfter, TBefore, TBy, TOn),
      TemporalConstraint (TemporalConstraint),
      mt2text,
      pt2text,
      rp2text,
    )
  import Text.Regex.PCRE.Heavy qualified as PCRE
  import Debug.Trace (trace)
  
  type Ann = ()
  
  taSysToString :: CoreL4.TASys () -> String
  taSysToString = show . showL4 [PrintSystem UppaalStyle]
  
  toL4TA :: [SFL4R.Rule] -> CoreL4.TASys ()
  toL4TA rules = foldr (addRule henceChannels) emptyTASys { channelsOfSys =  Set.toList henceChannels } rules
    where
      henceChannels = Set.fromList $ foldMap getHence rules
  
  getHence :: SFL4R.Rule -> [String]
  getHence Regulative{ hence = Just (RuleAlias rname)} = pure . unpack $ mt2text rname
  getHence _ = []
  -- TODO: Handle recursive Hence
  
  emptyTASys :: TASys ()
  emptyTASys
    = TASys
        {annotOfSys = (), nameOfTASys = "Unknown name", declsOfSys = [],
         channelsOfSys = [], automataOfSys = []}
  
  addRule :: Set.HashSet ChannelName -> SFL4R.Rule -> CoreL4.TASys () -> CoreL4.TASys ()
  addRule hc r@Regulative{rlabel = Just (_,_,lb)} ts | unpack lb `Set.member` hc = ts {automataOfSys = fst (ruleToTA r (Just lb)) : automataOfSys ts}
                                                     | otherwise = ts {automataOfSys = fst (ruleToTA r Nothing) : automataOfSys ts} -- TODO: Use the decls in snd
  addRule _hc _r ts = ts
  
  -- TODO Nested
  -- TODO Handle party
  
  -- TODO: Make it recursive to handle missing fields gracefully
  ruleToTA :: SFL4R.Rule -> Maybe TL.Text -> (TA (), [VarDecl ()])
  ruleToTA Regulative{rlabel, temporal = Just (TemporalConstraint tcmp time _unit), upon= upn , cond = Just cnd} _ = (TA
      { nameOfTA = rName
      , annotOfTA = ()
      , locsOfTA = [initialLoc, uponLoc, ifBranchOkLoc, successLoc, breachLoc, timeConstraintSatisfiedLoc]
      , clocksOfTA = [ruleTimer]
      , transitionsOfTA = [uponTransition, ifBranchTransition, successTransition, timeConstraintSatisfiedTransition, timeConstraintFailedTransition]
      , initialLocOfTA = initialLoc
      , invarsOfTA = []
      , labellingOfTA = []
      , urgentLocsOfTA = [] -- TODO: Use
      }, ifCondDecls)
    where
      rName = maybe "TODO_generate_unique_name" (unpack . thrd) rlabel
      ruleTimer = Clock [i|time#{rName}|]
      initialLoc = Loc "Initial"
      uponLoc = Loc [i|Upon_#{maybe "START" pt2varname upn}|] -- TODO: Make this urgent when supported
      uponTransition = (simpleTransition initialLoc uponLoc) {
                                   actionOfTransition = TransitionAction [ruleTimer] (Skip ())
                                   }
      ifBranchOkLoc = Loc "RuleTriggers"
      successLoc = Loc "Sucess"
      ifCond = boolStructRToExpr cnd
      ifCondDecls = extractDecls $ fv ifCond
      ifBranchTransition = (simpleTransition uponLoc ifBranchOkLoc) {
                                   guardOfTransition = TransitionGuard [] $ Just $ void ifCond
                                   }
      successTransition = (simpleTransition uponLoc successLoc) {
                                   guardOfTransition = TransitionGuard [] $ Just $ void $ notExpr ifCond
                                   }
      -- TODO: Handle Lest
      breachLoc = Loc "Breach"
      timeConstraintSatisfiedLoc = Loc "TimeConstraintSatisfied"
      timeConstraintSatisfiedTransition = (simpleTransition ifBranchOkLoc timeConstraintSatisfiedLoc) {
                                   guardOfTransition = TransitionGuard [ClConstr ruleTimer (mkCompar tcmp) (fromMaybe 1 time)] Nothing
                                   }
      timeConstraintFailedTransition = (simpleTransition ifBranchOkLoc breachLoc) {
                                   guardOfTransition = TransitionGuard [ClConstr ruleTimer (negateCompar $ mkCompar tcmp) (fromMaybe 1 time)] Nothing
                                   }
  ruleToTA r _ = trace [i|Unexpected rule type: #{r}|] (TA {..}, [])
    where
      annotOfTA = ()
      nameOfTA = ""
      locsOfTA = []
      transitionsOfTA = []
      initialLocOfTA = Loc ""
      urgentLocsOfTA = []
      clocksOfTA = []
      invarsOfTA = []
      labellingOfTA = []
  
  extractDecls :: Set.HashSet (Var (Tp ())) -> [VarDecl ()]
  extractDecls = map varToVarDecl . Set.toList
  
  varToVarDecl :: Var (Tp ()) -> VarDecl ()
  varToVarDecl (GlobalVar (QVarName t varName)) = VarDecl () varName t
  varToVarDecl _ = trace "varToVarDecl: Impossible" $ VarDecl () "" OkT
  
  mkCompar :: TComparison -> BComparOp
  mkCompar TBefore = BClte
  mkCompar TAfter = BCgte
  mkCompar TBy = BClte
  mkCompar TOn = BCeq
  -- mkCompar TVague = _
  mkCompar other = error [i|Unsupported time constraint: #{other}|]
  
  negateCompar :: BComparOp -> BComparOp
  negateCompar BCeq = BCne
  negateCompar BClt = BCgte
  negateCompar BClte = BCgt
  negateCompar BCgt = BClte
  negateCompar BCgte = BClt
  negateCompar BCne = BCeq
  
  pt2varname :: ParamText -> String
  pt2varname = toValidName  . unpack . pt2text
  
  rp2varname :: RelationalPredicate -> String
  rp2varname = toValidName  . unpack . rp2text
  
  boolStructPToExpr :: BoolStructP -> CoreL4.Expr (Tp ())
  boolStructPToExpr (AA.Leaf pt) = mkVarE . GlobalVar . QVarName BooleanT $ pt2varname pt
  boolStructPToExpr (AA.Not  x)  = notExpr (boolStructPToExpr x)
  boolStructPToExpr (AA.Any _maybeprepost xs)  = disjsExpr $ boolStructPToExpr <$> xs
  boolStructPToExpr (AA.All _maybeprepost xs)  = conjsExpr $ boolStructPToExpr <$> xs
  
  boolStructRToExpr :: BoolStructR -> CoreL4.Expr (Tp ())
  boolStructRToExpr (AA.Leaf rp) = mkVarE . GlobalVar . QVarName BooleanT $ rp2varname rp
  boolStructRToExpr (AA.Not  bs)  = notExpr (boolStructRToExpr bs)
  boolStructRToExpr (AA.Any _maybeprepost xs)  = disjsExpr $ boolStructRToExpr <$> xs
  boolStructRToExpr (AA.All _maybeprepost xs)  = conjsExpr $ boolStructRToExpr <$> xs
  
  simpleTransition :: Loc -> Loc -> Transition ()
  simpleTransition src tgt = Transition { sourceOfTransition = src
                                         , targetOfTransition = tgt
                                         , guardOfTransition = TransitionGuard [] Nothing
                                         , syncOfTransition = Nothing
                                         , actionOfTransition = TransitionAction [] (Skip ())
                                         }
  
  thrd :: RuleLabel -> TL.Text
  thrd (_,_,t) = t
  
  toValidName :: [Char] -> [Char]
  toValidName = PCRE.gsub [PCRE.re| \(|\)|§|] "_"
      -- underscorize ' ' = '_'
      -- underscorize '(' = '_'
      -- underscorize ')' = '_'
      -- underscorize '§' = '_'
      -- underscorize c = c
  
  
  
  {-
  - Identify automata
  - Identify channels
  
  - Look into automata
  - Difficult: Figure out states
  
  Q: Global clock?
  
  "Within X time" means "Reset timer when entering this state, Exit condition when leaving state"
  
  -}
  
  -- data Rule = Regulative
  --             { subj     :: BoolStrucPt               -- man AND woman AND child
  --             , keyword  :: MyToken                   -- Every | Party | TokAll
  --             , who      :: Maybe BoolStructP         -- who walks and (eats or drinks)
  --             , cond     :: Maybe BoolStructP         -- if it is a saturday
  --             , deontic  :: Deontic            -- must
  --             , action   :: BoolStructP          -- fart loudly AND run away
  --             , temporal :: Maybe (TemporalConstraint Text.Text) -- Before "midnight"
  --             , hence    :: Maybe Rule
  --             , lest     :: Maybe Rule
  --             , rlabel   :: Maybe RuleLabel
  --             , lsource  :: Maybe Text.Text
  --             , srcref   :: Maybe SrcRef
  --             , upon     :: [BoolStructP] -- UPON entering the club (event prereq trigger)
  --             , given    :: Maybe ParamText
  --             , having   :: Maybe ParamText  -- HAVING sung...
  --             , orig     :: [(Preamble, BoolStructP)]
  --             }
  --           | Constitutive
  --             { name     :: ConstitutiveName   -- the thing we are defining
  --             , keyword  :: MyToken       -- Means, Includes, Is, Deem
  --             , letbind  :: BoolStructP   -- might be just a bunch of words to be parsed downstream
  --             , cond     :: Maybe BoolStructP -- a boolstruct set of conditions representing When/If/Unless
  --             , given    :: Maybe ParamText
  --             , rlabel   :: Maybe RuleLabel
  --             , lsource  :: Maybe Text.Text
  --             , srcref   :: Maybe SrcRef
  --             , orig     :: [(Preamble, BoolStructP)]
  --             }
  --           | TypeDecl
  --             { name     :: ConstitutiveName  --      DEFINE Sign
  --             , super    :: Maybe TypeSig     --                  :: Thing
  --             , has      :: Maybe [ParamText] -- HAS foo :: List Hand \n bar :: Optional Restaurant
  --             , enums    :: Maybe ParamText   -- ONE OF rock, paper, scissors (basically, disjoint subtypes)
  --             , rlabel   :: Maybe RuleLabel
  --             , lsource  :: Maybe Text.Text
  --             , srcref   :: Maybe SrcRef
  --             }
  --           | DefNameAlias -- inline alias, like     some thing AKA Thing
  --             { name   :: ConstitutiveName   -- "Thing" -- the thing usually said as ("Thing")
  --             , detail :: BoolStructP        -- "some thing"
  --             , nlhint :: Maybe Text.Text  -- "lang=en number=singular"
  --             , srcref :: Maybe SrcRef
  --             }
  --           | RuleAlias Text.Text -- internal softlink to a rule label (rlabel), e.g. HENCE NextStep
  --           | RuleGroup { rlabel :: Maybe RuleLabel }  -- § NextStep
  --           | RegFulfilled  -- trivial top
  --           | RegBreach     -- trivial bottom
  