-- renaming is not supported yet
{
addReductionPopupItems :: [ PopupMenuItem doc enr node clip token ] -> Presentation doc enr node clip token -> Presentation doc enr node clip token
addReductionPopupItems its pres = addPopupItems pres its

pasteExp :: [Int] -> Exp -> UpdateDoc Document clip
pasteExp pth exp =
  \(DocumentLevel d path cl) ->
    let (DocumentLevel d' _ _) = editPasteD (DocumentLevel d (PathD pth)
                                              (Clip_Exp exp)
                                            )
    in  (DocumentLevel d' path cl)


setIDPExp newIdp (PlusExp idp0 x1 x2)           = PlusExp newIdp x1 x2
setIDPExp newIdp (TimesExp idp x1 x2)           = TimesExp newIdp x1 x2
setIDPExp newIdp (DivExp idp0 x1 x2)            = DivExp idp0 x1 x2
setIDPExp newIdp (PowerExp idp0 x1 x2)          = PowerExp newIdp x1 x2
setIDPExp newIdp (BoolExp idp0 x1)              = BoolExp newIdp x1
setIDPExp newIdp (IntExp idp0 x1)               = IntExp newIdp x1
setIDPExp newIdp (CaseExp idp0 idp1 x1 x2)       = CaseExp newIdp idp1 x1 x2
setIDPExp newIdp (LetExp idp0 idp1 dcls x2)     = LetExp newIdp idp1 dcls x2
setIDPExp newIdp (LamExp idp0 idp1 x1 x2)       = LamExp newIdp idp1 x1 x2
setIDPExp newIdp (AppExp x1 x2)                 = AppExp (setIDPExp newIdp x1) x2  -- has no pid of its own
setIDPExp newIdp (IdentExp x1)                  = IdentExp (setIDPIdent newIdp x1) -- has no pid of its own
setIDPExp newIdp (IfExp idp0 idp idp1 x1 x2 x3) = IfExp newIdp idp idp1 x1 x2 x3
setIDPExp newIdp (ParenExp idp0 idp1 x1)        = ParenExp newIdp idp1 x1
setIDPExp newIdp (ListExp idp0 idp1 idps x1)    = ListExp newIdp idp1 idps x1
setIDPExp newIdp (ProductExp idp0 idp1 idps x1) = ProductExp newIdp idp1 idps x1
setIDPExp _   exp                               = exp

setIDPIdent newIdp (Ident idp0 idp1 str) = Ident newIdp idp1 str

removeParens (ParenExp _ _ x1) = removeParens x1
removeParens exp               = exp

ensureParens exp = ParenExp NoIDP NoIDP (removeParens exp)
}

-- The explicit parenthesis style of Helium makes reduction a bit tricky.
-- If they are removed, the document may change when the presentation is parsed  "(\...) ..."   => "\... ..."
-- therefore, disregard parentheses during reduction

SEM Exp
  | PlusExp
      loc.reductionEdit = case (removeParens @exp1.self, removeParens @exp2.self) of
                                 (IntExp idp1 int1, IntExp _ int2) -> [ ("Reduce primitive (+)" , docUpd $ pasteExp @lhs.path (IntExp idp1 (int1+int2)))]
                                 _                                   -> []
  | TimesExp
      loc.reductionEdit = case (removeParens @exp1.self, removeParens @exp2.self) of
                                 (IntExp idp1 int1, IntExp _ int2) -> [ ("Reduce primitive (*)" , docUpd $ pasteExp @lhs.path (IntExp idp1 (int1*int2)))]
                                 _                                   -> []
  | DivExp
      loc.reductionEdit = case (removeParens @exp1.self, removeParens @exp2.self) of
                                 (IntExp idp1 int1, IntExp _ int2) -> [ ("Reduce primitive div" , docUpd $ pasteExp @lhs.path (IntExp idp1 (int1 `div` int2)))]
                                 _                                   -> []
  | PowerExp
      loc.reductionEdit = case (removeParens @exp1.self, removeParens @exp2.self) of
                                 (IntExp idp1 int1, IntExp _ int2) -> [ ("Reduce primitive (^)" , docUpd $ pasteExp @lhs.path (IntExp idp1 (int1^int2)))]
                                 _                                   -> []
  | AppExp -- pattern matching is not ok in ag
      loc.reductionEdit = case removeParens @exp1.self of
                                  LamExp _ _ ident exp -> [ ("Beta reduce",
                                                             docUpd $ pasteExp @lhs.path
                                                                      (ensureParens (@exp1.lamBody [(strFromIdent ident, @exp2.self)] ))
                                                            )
                                                          ]
                                  _                    -> []
  | IdentExp  -- only for top level, until it is clear how to do let expressions
      loc.reductionEdit =  case Map.lookup (strFromIdent @ident.self) @lhs.varsInScope of
                             Nothing      -> []
                             Just (PathD pth@(_:_),_) ->
                               [( "Replace by definition"
                                , docUpd $ 
                                  \(DocumentLevel d path cl) ->
                                  case selectD (init pth) d of -- pattern matched, so pth is not null
                                    (Clip_Decl (Decl idP0 idP1 idP2 idP3 _ _ _ exp)) ->
                                          let (DocumentLevel d' _ _) =
                                                editPasteD (DocumentLevel d (PathD @lhs.path) (Clip_Exp ( setIDPExp (idP0FromIdent @ident.self) $ ensureParens exp)))
                                          in  (DocumentLevel d' path cl)
                                    _ -> (DocumentLevel d path cl)
                                )] -- The menu now also appears for idents refering to lambda vars. A nicer
                                   -- impl. needs a select function in the ag, or an inh. root doc attr so selectD can be used
                                   -- differences between enriched and doc become should be taken into account then

                -- pth is path of ident, path is current doc focus and @lhs.path is path to identExp
  | IfExp
      loc.reductionEdit = case removeParens @exp1.self of
                                 BoolExp _ bool -> [("Reduce primitive if" , docUpd $ pasteExp @lhs.path
                                                                                          (if bool then setIDPExp @idP0 @exp2.self
                                                                                                   else setIDPExp @idP0 @exp3.self))]
                                 _                          -> []
  | BoolExp IntExp LamExp CaseExp LetExp ParenExp ListExp ProductExp
      loc.reductionEdit = [] -- cannot be reduced

{- CaseExp   -- Case only matches on variables so reducing is rather useless
   LetExp    -- have to think about this one
   ParenExp loc.reductionEdit = [] -- ("Remove parens" , docUpd $ pasteExp @lhs.path @exp.self)]
-}

-- need higher order ag here
SEM Exp [|| substitute :{( [(String, Exp)] -> Exp )}]
  | PlusExp
      loc.substitute = \substs -> PlusExp @idP0 (@exp1.substitute substs) (@exp2.substitute substs)
  | TimesExp
      loc.substitute = \substs -> TimesExp @idP0 (@exp1.substitute substs) (@exp2.substitute substs)
  | DivExp
      loc.substitute = \substs -> DivExp @idP0 (@exp1.substitute substs) (@exp2.substitute substs)
  | PowerExp
      loc.substitute = \substs -> PowerExp @idP0 (@exp1.substitute substs) (@exp2.substitute substs)
  | LamExp --   filter substs
      loc.substitute = \substs -> LamExp @idP0 @idP1 @ident.self (@exp.substitute
                                                                        (filter (\(str,_) -> str /= strFromIdent @ident.self)
                                                                                substs))
  | AppExp
      loc.substitute = \substs -> AppExp (@exp1.substitute substs) (@exp2.substitute substs)
  | IdentExp
      loc.substitute = \substs -> case lookup (strFromIdent @ident.self) substs of -- parseErr & hole give ""
                                          Just exp -> exp
                                          Nothing  -> @self
  | IfExp
      loc.substitute = \substs -> IfExp @idP0 @idP1 @idP2 (@exp1.substitute substs) (@exp2.substitute substs) (@exp3.substitute substs)
  | ParenExp
      loc.substitute = \substs -> ParenExp @idP0 @idP1 (@exp.substitute substs)

  | BoolExp IntExp CaseExp LetExp ListExp ProductExp HoleExp ParseErrExp
      loc.substitute = \substs -> @self


SEM Exp [|| lamBody : {([(String, Exp)] -> Exp)} ]
  | LamExp
      lhs.lamBody = @exp.substitute
  | ParenExp
      lhs.lamBody = @exp.lamBody
  | PlusExp TimesExp DivExp PowerExp BoolExp IntExp AppExp CaseExp LetExp
            IdentExp IfExp ListExp ProductExp HoleExp ParseErrExp
      lhs.lamBody = @substitute

{-

--

-- ATTR Exp [ reductionEdit :: {[PopupItem]} || ]

-- SEM Plus  reductionEdit =
        if left and right are int then Int + right

-- SEM Ident
       if lookup yields path, then substitute exp at path for IdentExp (use new doc ids!!)


-- SEM Apply fn arg
      only if fn == Lambda id -> exp
      substitute all free occ. of id for arg


Issues:
Only substitute free variables
(\y -> (\y -> y) ) x
wrong:  (\y -> x)
right: (\y -> y)

Rename when free variable is captured:
(\y -> (\x -> y) ) x
wrong: (\x -> x)
right: (\x' -> x)

attr subst. tree :: [bindings ] -> tree


Let dcls exp: \substs -> Let dcls (exp.subst (remove dcls from substs))
Lambda param body: \substs -> Lambda param (body.subst (remove param from substs))
Rest is simple

How to avoid capturing? x := exp
Also pass freevars from exp, and if let decl or arg is freevar, rename it uniquely to something not in freevar or freevar of exp

Lambda param body \substs, freevars -> Lambda let param' =
                                                                        in exp.subst (remove param from substs ++ if param is in freevar then [param := new param] else []

subst is not recursive [x = y, y =2] x is y and not 2, otherwise we need HAG

-}