content: {-# LANGUAGE TypeFamilies, DeriveAnyClass, DeriveGeneric, OverloadedStrings #-}
  module Rule where
  import qualified ProofTree as PT
  import qualified Prop as P
  import qualified Terms as T
  import Controller
  import Unification
  import Debug.Trace
  import Miso.String (MisoString, pack)
  import Data.String
  import qualified Miso.String as MS
  import Optics.Core
  import StringRep
  import qualified Data.Char
  import Control.Monad(when)
  import Data.Maybe(fromMaybe,fromJust,mapMaybe)
  import Data.List
  import GHC.Generics(Generic)
  import Data.Aeson (ToJSON,FromJSON)
  import qualified Data.Map as M
  data RuleType
    = Axiom
    | Theorem
    | Inductive
    deriving (Show, Eq, Generic, ToJSON, FromJSON)
  
  data RuleItem = RI P.RuleName P.Prop (Maybe ProofState)
    deriving (Show, Eq, Generic, ToJSON, FromJSON)
  data Rule = R RuleType [RuleItem] [P.NamedProp]
    deriving (Show, Eq, Generic, ToJSON, FromJSON)
  
  type Counter = Int
  data ProofState = PS PT.ProofTree Counter
    deriving (Show, Eq, Generic, ToJSON, FromJSON)
  
  name :: Lens' RuleItem P.RuleName
  name = lensVL $ \act (RI n prp m) -> (\n' -> RI n' prp m) <$> act n
  
  blank :: RuleType -> P.RuleName -> Rule
  blank Axiom n = (R Axiom [RI n P.blank Nothing] [])
  blank Inductive n = (R Inductive [RI n P.blank Nothing] [])
  blank Theorem n = (R Theorem [RI n P.blank (Just $ PS (PT.fromProp P.blank) 0)] [])
  
  ruleItems :: IxTraversal' Int Rule RuleItem 
  ruleItems = itraversalVL guts
    where 
      guts f (R t ls rest) =  R t <$> traverse (\(i, e) -> f i e) (zip [0..] ls) <*> pure rest
  
  deleteItemFromRI :: Int -> [RuleItem] -> [RuleItem]
  deleteItemFromRI _ [] = []
  deleteItemFromRI n ris = left ++ right
    where
      (left , x:right) = splitAt n ris
      
    
  -- warning, do not use this lens to assign to anything that might invalidate the proof state
  -- use propUpdate for that (which will reset the proof state)
  prop :: Lens' RuleItem P.Prop
  prop = lensVL $ \act (RI n prp m) -> (\prp' -> RI n prp' m) <$> act prp
  
  -- disjoint product of prop and name
  namedProp :: Lens' RuleItem P.NamedProp
  namedProp = lensVL $ \act (RI n prp m) -> (\(P.Defn n',prp') -> RI n' prp' m) <$> act (P.Defn n, prp)
  
  propUpdate :: Setter' RuleItem P.Prop
  propUpdate = sets guts
    where
      guts act (RI n p s)
        | p' <- act p
        = RI n p' (fmap (const $ PS (PT.fromProp p') 0) s)
  
  proofState :: AffineTraversal' RuleItem ProofState
  proofState =  atraversal
    (\i   -> case i of RI _ _ (Just s) -> Right s
                       i -> Left i)
    (\i s -> case i of RI n p (Just _) -> RI n p (Just s)
                       i -> i)
  
  
  applyRewriteTactic :: RuleItem  -> P.NamedProp -> Bool -> PT.Path -> Maybe RuleAction
  applyRewriteTactic state np rev pth = 
    case traverseOf proofState (runUnifyPS $ PT.applyRewrite np rev pth) state of
       Left _ -> Nothing
       Right st' -> flip Tactic pth <$> preview proofState st'
  applyERuleTactic :: RuleItem -> P.NamedProp -> P.NamedProp -> PT.Path -> Maybe RuleAction
  applyERuleTactic state assm np pth = 
    case traverseOf proofState (runUnifyPS $ PT.applyElim np pth assm) state of
       Left _ -> Nothing 
       Right st' -> flip Tactic pth <$> preview proofState st'
  
  
  applyRuleTactic :: RuleItem -> P.NamedProp -> PT.Path -> Maybe RuleAction
  applyRuleTactic state  np pth = 
    case traverseOf proofState (runUnifyPS $ PT.apply np pth) state of
       Left _ -> Nothing
       Right st' -> flip Tactic pth <$> preview proofState st'
  
  unresolved :: ProofState -> Bool
  unresolved (PS pt c) = has PT.outstandingGoals pt
  
  proofTree :: Lens' ProofState PT.ProofTree
  proofTree = lensVL $ \act (PS pt c) -> flip PS c <$> act pt
  
  runUnifyPS :: (PT.ProofTree -> UnifyM PT.ProofTree) -> ProofState -> Either UnifyError ProofState
  runUnifyPS act (PS pt c) = case runUnifyM (act pt) c of
                               (Left e, c) -> Left e
                               (Right pt',c') -> Right (PS pt' c')
  
  checkVariableName :: MS.MisoString -> Controller f ()
  checkVariableName new = case T.invalidName new of
    Just e  -> errorMessage $ "Invalid variable name: " <> pack e
    Nothing -> pure ()
  
  data ProofFocus = GoalFocus Bool [(P.NamedProp, RuleAction)]  -- bool is whether to show non-intro rules
                  | RewriteGoalFocus Bool [(P.NamedProp, RuleAction)] -- bool is rewrite direction
                  | AssumptionFocus Int [(P.NamedProp, RuleAction)]
                  | MetavariableFocus Int
                  | SubtitleFocus PT.Path
                  | ProofBinderFocus PT.Path Int deriving (Show, Eq)
  
  data GoalSummary = GS [(PT.Path,Int,T.Name)] [(P.NamedProp, Maybe RuleAction)] T.Term PT.Path Bool deriving (Show, Eq)
  
  getGoalSummary :: RuleItem -> PT.Path -> Maybe GoalSummary
  getGoalSummary state' f = GS <$> pure (associate state' f)
                                   <*> fmap (map tryApply . zip (map P.Local [0 ..]) . PT.locals . fst)  (ipreview (PT.path f PT.%+ PT.step) =<< preview (proofState % proofTree) state')
                                   <*> preview (proofState % proofTree % PT.path f % PT.inference) state' 
                                   <*> pure f <*> pure False
    where 
      tryApply r = (r,  applyRuleTactic state' r f)
      associate (RI _ _ (Just (PS pt _))) f = go [] (reverse f) pt
      go pth [] pt = zipWith (\i n -> (pth, i, n)) [0..] (view PT.goalbinders pt)
      go pth (x:xs) pt = zipWith (\i n -> (pth, i, n)) [0..] (view PT.goalbinders pt) ++ case preview (PT.subgoal x) pt of 
                           Nothing -> [] 
                           Just sg -> go (x:pth) xs sg 
  
  data RuleFocus = ProofFocus ProofFocus (Maybe GoalSummary)
                    | RuleBinderFocus P.Path Int
                    | NewRuleBinderFocus P.Path
                    | RuleTermFocus P.Path
                    | NameFocus
                    deriving (Show, Eq)
  
  data RuleAction = Tactic ProofState PT.Path
                    | SetStyle PT.Path PT.ProofStyle
                    | SetSubgoalHeading PT.Path
                    | Nix PT.Path
                    | NormaliseEquality PT.Path
                    | SelectGoal PT.Path Bool -- bool is to show non-intro rules or not
                    | ExamineAssumption Int
                    | RewriteGoal Bool
                    | RenameProofBinder PT.Path Int
                    | AddRuleBinder P.Path
                    | RenameRuleBinder P.Path Int
                    | DeleteRuleBinder P.Path Int
                    | UpdateTerm P.Path
                    | AddPremise P.Path
                    | DeletePremise P.Path
                    | Rename
                    | InstantiateMetavariable Int
                    | DeleteRI  
                    deriving (Show, Eq)
  
  
  editableRI tbl (ProofFocus (ProofBinderFocus pth i) g) = preview (proofState % proofTree % PT.path pth % PT.goalbinders % ix i)
  editableRI tbl (RuleBinderFocus pth i) = preview (prop % P.path pth % P.metabinders % ix i)
  editableRI tbl (RuleTermFocus pth) = Just . P.getConclusionString tbl pth . view prop
  editableRI tbl (ProofFocus (MetavariableFocus i) g) = const (Just ("?" <> pack (show i)))
  editableRI tbl NameFocus = preview name
  editableRI tbl (ProofFocus (SubtitleFocus pth) g) = fmap (fromMaybe "Show:" . fmap PT.subtitle) . preview (proofState % proofTree % PT.path pth % PT.displaydata)
  editableRI _ _ = const Nothing
  
  leaveFocusRI (ProofFocus (ProofBinderFocus p i) g) = noFocus . handleRI (RenameProofBinder p i) --These define the action when the user leaves focus on an item
  leaveFocusRI (RuleBinderFocus p i)  = noFocus . handleRI (RenameRuleBinder p i)
  leaveFocusRI (NewRuleBinderFocus p) = noFocus . handleRI (AddRuleBinder p)
  leaveFocusRI (RuleTermFocus p)      = noFocus . handleRI (UpdateTerm p)
  leaveFocusRI NameFocus              = noFocus . handleRI Rename
  --TODO handle other foci?
  leaveFocusRI _                      = pure
  
  
  distinctness :: P.NamedProp -> Maybe P.NamedProp
  distinctness (n, P.Forall xs [] (T.Ap (T.Ap (T.Const "_=_" False) a) b)) 
    | (T.Const a' True, avs) <- T.peelApTelescope a
    , (T.Const b' True, bvs) <- T.peelApTelescope b
    = if a' /= b' || length avs /= length bvs then 
        Just (P.Distinctness n, P.Forall ["P"] [] (T.LocalVar 0))
      else Nothing 
  distinctness _ = Nothing
  
  
  injectivity :: P.NamedProp -> Maybe P.NamedProp
  injectivity (n, asm@(P.Forall [] [] (T.Ap (T.Ap (T.Const "_=_" False) a) b)))
    | (T.Const a' True, avs) <- T.peelApTelescope a
    , (T.Const b' True, bvs) <- T.peelApTelescope b
    = if a' == b' && length avs == length bvs then 
        Just (P.Injectivity, P.Forall ["P"] (P.raise 1 asm: [ P.Forall [] (zipWith (\v1 v2 -> P.Forall [] [] $ T.raise 1 $ T.Ap (T.Ap (T.Const "_=_" False) v1) v2) avs bvs) (T.LocalVar 0) ] ) (T.LocalVar 0) )
      else Nothing 
  injectivity _ = Nothing
  handleRI :: RuleAction -> RuleItem -> Controller RuleFocus RuleItem
  
  handleRI (SelectGoal pth b) state = do
      let summary = getGoalSummary state pth 
      rules <- filter (if b then const True else P.isIntroduction . snd) <$> getKnownRules
      setFocus (ProofFocus (GoalFocus b $ mapMaybe (\r -> (,) r <$> applyRuleTactic state r pth) rules) summary)
      pure state
  handleRI (ExamineAssumption i) state = do 
    foc <- getOriginalFocus 
    case foc of 
      Just (ProofFocus _ (Just gs@(GS _ lcls _ p _))) | (it:_) <- drop i lcls -> do
        case distinctness (fst it) of
          Just rule | Just a <- applyRuleTactic state rule p -> handleRI a state
          _ -> case injectivity (fst it) of 
            Just rule | Just a <- applyERuleTactic state (fst it) rule p -> handleRI a state
            _ -> do
              rules <- getKnownRules
              setFocus (ProofFocus (AssumptionFocus i (mapMaybe (\r -> (,) r <$> applyERuleTactic state (fst it) r p) rules)) (Just gs))
              pure state
      _ -> pure state
  handleRI (RewriteGoal rev) state = do 
    foc <- getOriginalFocus 
    case foc of 
      Just (ProofFocus _ (Just gs@(GS _ lcls t p _)))  ->
        case applyRuleTactic state P.builtInRefl p of 
          Just a -> handleRI a state
          Nothing -> do
            rules <- filter (P.isRewrite . snd) . (map fst lcls ++) <$> getKnownRules
            setFocus (ProofFocus (RewriteGoalFocus rev (mapMaybe (\r -> (,) r <$> applyRewriteTactic state r rev p ) rules)) (Just gs))
            pure state
      _ -> pure state
  handleRI (Tactic ps pth) state = let 
          state' = set proofState ps state 
          newFocus = if has (proofState % proofTree % PT.path (0:pth)) state'
                      then Just (0:pth)
                      else fst <$> ipreview (isingular (proofState % proofTree % PT.outstandingGoals)) state'
        in do
          case newFocus of
            Just f -> handleRI (SelectGoal f False) state'
            _      -> clearFocus >> pure state'
  handleRI (SetStyle pth st) state = do
    let f Nothing = Just (PT.PDD { PT.style = st, PT.subtitle = "Show:" })
        f (Just pdd) = Just $ pdd { PT.style = st}
    pure $ over (proofState % proofTree % PT.path pth % PT.displaydata) f state
  handleRI (SetSubgoalHeading pth) state = do
    new <- textInput
    let f Nothing = Just (PT.PDD {  PT.style = PT.Tree, PT.subtitle = new })
        f (Just pdd) = Just $ pdd { PT.subtitle = new }
    foc <- getOriginalFocus
    let state' = over (proofState % proofTree % PT.path pth % PT.displaydata) f state
    case foc of
      Just (ProofFocus _ (Just (GS _ _ _ p _))) -> handleRI (SelectGoal p False) state'
      _ -> pure state'
  handleRI (Nix pth) state = do
      clearFocus
      pure $ over (proofState % proofTree % PT.path pth) PT.nix state
  
  handleRI (RenameProofBinder pth i) state = do
      new <- textInput
      checkVariableName new
      let state' = set (proofState % proofTree % PT.path pth % PT.goalbinders % ix i) new state
      foc <- getOriginalFocus
      case foc of
        Just (ProofFocus _ (Just (GS _  _ _ p _))) -> handleRI (SelectGoal p False) state'
        _ -> pure state'
  
  handleRI (AddRuleBinder pth) state = do
      new <- textInput
      let news = filter (not . MS.null) (MS.splitOn "." new)
      mapM checkVariableName news
      invalidate (view name state)
      setFocus (RuleTermFocus pth)
      pure $ over (propUpdate % P.path pth) (P.addBinders news) state
  
  handleRI (RenameRuleBinder pth i) state = do
      new <- textInput
      checkVariableName new
      clearFocus -- should it be updateterm?
      pure $ set (prop % P.path pth % P.metabinders % ix i) new state
  
  handleRI (NormaliseEquality p) state = 
      pure $ over (proofState % proofTree) (PT.normaliseEquality p) state
  handleRI (DeleteRuleBinder pth i) state = do
      when (maybe False (P.isBinderUsed i) $ preview (prop % P.path pth) state) $ errorMessage "Cannot remove binder: is in use"
      invalidate (view name state)
      clearFocus
      pure $ over (propUpdate % P.path pth) (P.removeBinder i) state
  
  handleRI (UpdateTerm pth) state = do
      new <- textInput
      tbl <- syntaxTable
      case toLensVL prop (P.setConclusionString tbl pth new) state of
        Left e -> errorMessage $ "Parse error: " <> e
        Right state' -> do
          invalidate (view name state')
          case pth of [] -> clearFocus
                      (_:pth') -> setFocus (RuleTermFocus pth')
          pure $ over propUpdate id state' --hack..
  handleRI (InstantiateMetavariable i) state = do
    new <- textInput
    tbl <- syntaxTable
    case parse tbl [] new of
      Left e -> errorMessage $ "Parse error: " <> e
      Right obj -> do
          foc <- getOriginalFocus
          let state' = over (proofState % proofTree) (PT.applySubst (T.fromUnifier [(i,obj)])) state
          case foc of
            Just (ProofFocus _ (Just (GS _  _ _ p _))) -> handleRI (SelectGoal p False) state'
            _ -> pure state'
  
  handleRI (AddPremise pth) state = do
      invalidate (view name state)
      let newIndex = length $ fromMaybe [] (preview (prop % P.path pth % P.premises) state)
      setFocusWithLeaving (RuleTermFocus (newIndex:pth))
      pure $ over (propUpdate % P.path pth % P.premises) (++[P.blank]) state
  
  handleRI (DeletePremise []) state = pure state -- shouldn't happen
  handleRI (DeletePremise (x:pth)) state = do
      invalidate (view name state)
      setFocus (RuleTermFocus (pth))
      pure $ over (propUpdate % P.path pth) (P.removePremise x) state
  
  handleRI Rename state = do
      new <- textInput
      when (new == "") $ errorMessage "Name cannot be empty"
      when (MS.all Data.Char.isSpace new) $ errorMessage "Name cannot be empty"
      renameResource (view name state) new
      clearFocus
      pure $ set name new state
  
  generateDerivedRules :: [P.RuleName] -> RuleType -> [RuleItem] -> Controller (Focus Rule) [P.NamedProp]
  generateDerivedRules old Inductive rs = 
    let rs' = filter P.isIntroduction (map (view prop) rs)
        definitions = foldr (\x m -> M.insertWith (++) (P.introRoot x) [x] m) M.empty rs'
        caseRules = map snd $ M.toList $ M.mapWithKey (\(k,i) intros -> P.caseRule k i intros) definitions
        allIntros = concatMap snd $ M.toList definitions
        inductionRules = map snd $ M.toList $ M.mapWithKey (\(k,i) intros -> P.inductionRule k i (M.keys definitions) allIntros) definitions
        newRules = caseRules ++ inductionRules
     in do generateDiffs old (mapMaybe (P.defnName . fst) newRules) 
           pure newRules 
    where 
      generateDiffs old [] = mapM_ invalidate old
      generateDiffs old (n:ns) | n `notElem` old = newResource n >> generateDiffs old ns
                               | otherwise = generateDiffs old ns
  generateDerivedRules _ _ _ = pure []
  
  instance Control Rule where
    data Focus Rule = RF Int RuleFocus
                    | AddingRule
                    deriving (Show, Eq)
  
    data Action Rule = RA Int RuleAction
                     | AddRule
                     deriving (Show, Eq)
  
    defined (R _ ls rest) = map (\(RI n prp _) -> (P.Defn n,prp) ) ls ++ rest
  
    inserted _ = RF 0 (RuleTermFocus [])
  
    invalidated s r = over (ruleItems % proofState % proofTree) (PT.clear s) r
  
    renamed (s,s') r = over (ruleItems % proofState % proofTree) (PT.renameRule (s,s')) r
  
    editable tbl (RF i rf) (R _ ls _) = editableRI tbl rf (ls !! i)
    editable tbl AddingRule _ = Nothing
  
    leaveFocus (RF i rf) r = atraverseOf (elementOf ruleItems i) pure (leaveFocusRI rf) r
    leaveFocus AddingRule r = pure r
  
    handle (RA i DeleteRI) r@(R ruleType lst rest) = do
      let (left , x:right) = splitAt i lst
      let ruleName = view name x
      invalidate ruleName
      rest' <- generateDerivedRules (mapMaybe (P.defnName . fst) rest) ruleType (left ++ right)
      pure (R ruleType (left ++ right) rest')
  
    handle (RA i a) r = do
      R t sgs rest <- zoomFocus (RF i) (\(RF i' rf) -> if i == i' then Just rf else Nothing) 
                                       (atraverseOf (elementOf ruleItems i) pure (handleRI a) r)
      b <- anyInvalidated 
      if b then do 
        rest' <- generateDerivedRules (mapMaybe (P.defnName . fst) rest) t sgs
        pure (R t sgs rest')
      else pure (R t sgs rest)
      
    handle AddRule (R t ls rest) = do
      name <- textInput
      newResource name
      rest' <- generateDerivedRules (mapMaybe (P.defnName . fst) rest) t (ls ++ [RI name P.blank Nothing]) 
      let s' = R t (ls ++ [RI name P.blank Nothing]) rest'
      setFocus (RF (length ls) $ RuleTermFocus [])
      pure s'
  