module TTImp.Interactive.GenerateDef -- Attempt to generate a complete definition from a type import Core.Contextimport Core.Envimport Core.Metadataimport Core.Normaliseimport Core.TTimport Core.Unifyimport Core.Value import Parser.Lexer import TTImp.Elabimport TTImp.Elab.Checkimport TTImp.Interactive.CaseSplitimport TTImp.Interactive.ExprSearchimport TTImp.ProcessDeclsimport TTImp.ProcessDefimport TTImp.TTImpimport TTImp.Unelabimport TTImp.Utils %default covering fnName : Bool -> Name -> StringfnName lhs (UN n)    = if isIdentNormal n then n      else if lhs then "(" ++ n ++ ")"      else "op"fnName lhs (NS _ n) = fnName lhs nfnName lhs (DN s _) = sfnName lhs n = show n -- Make the hole on the RHS have a unique nameuniqueRHS : {auto c : Ref Ctxt Defs} ->            ImpClause -> Core ImpClauseuniqueRHS (PatClause fc lhs rhs)    = pure $ PatClause fc lhs !(mkUniqueName rhs)  where    mkUniqueName : RawImp -> Core RawImp    mkUniqueName (IHole fc' rhsn)        = do defs <- get Ctxt             rhsn' <- uniqueName defs [] rhsn             pure (IHole fc' rhsn')    mkUniqueName tm = pure tm -- it'll be a hole, but this is needed for coveringuniqueRHS c = pure c expandClause : {auto c : Ref Ctxt Defs} ->               {auto m : Ref MD Metadata} ->               {auto u : Ref UST UState} ->               FC -> Int -> ImpClause ->               Core (List ImpClause)expandClause loc n c    = do log 10 $ "Trying clause " ++ show c         c <- uniqueRHS c         Right clause <- checkClause linear False n [] (MkNested []) [] c            | Left _ => pure [] -- TODO: impossible clause, do something                                -- appropriate         let MkClause {vars} env lhs rhs = clause         logTerm 10 "RHS hole" rhs         let Meta _ i fn _ = getFn rhs            | _ => throw (GenericMsg loc "No searchable hole on RHS")         defs <- get Ctxt         Just (Hole locs _) <- lookupDefExact (Resolved fn) (gamma defs)            | _ => throw (GenericMsg loc "No searchable hole on RHS")         log 10 $ "Expression search for " ++ show (i, fn)         (rhs' :: _) <- exprSearch loc (Resolved fn) []            | _ => throw (GenericMsg loc "No result found for search on RHS")         defs <- get Ctxt         rhsnf <- normaliseHoles defs [] rhs'         let (_ ** (env', rhsenv)) = dropLams locs [] rhsnf          rhsraw <- unelab env' rhsenv         logTermNF 5 "Got clause" env lhs         logTermNF 5 "        = " env' rhsenv         pure [updateRHS c rhsraw]  where    updateRHS : ImpClause -> RawImp -> ImpClause    updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs    -- 'with' won't happen, include for completeness    updateRHS (WithClause fc lhs wval cs) rhs = WithClause fc lhs wval cs    updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs     dropLams : Nat -> Env Term vars -> Term vars ->               (vars' ** (Env Term vars', Term vars'))    dropLams Z env tm = (_ ** (env, tm))    dropLams (S k) env (Bind _ _ b sc) = dropLams k (b :: env) sc    dropLams _ env tm = (_ ** (env, tm)) splittableNames : RawImp -> List NamesplittableNames (IApp _ f (IBindVar _ n))    = splittableNames f ++ [UN n]splittableNames (IApp _ f _)    = splittableNames fsplittableNames (IImplicitApp _ f _ _)    = splittableNames fsplittableNames _ = [] trySplit : {auto m : Ref MD Metadata} ->           {auto c : Ref Ctxt Defs} ->           {auto u : Ref UST UState} ->           FC -> RawImp -> ClosedTerm -> RawImp -> Name ->           Core (Name, List ImpClause)trySplit loc lhsraw lhs rhs n    = do OK updates <- getSplitsLHS loc 0 lhs n            | _ => pure (n, [])         pure (n, map (\ups => PatClause loc (updateLHS ups lhsraw) rhs)                      (mapMaybe valid updates))  where    valid : ClauseUpdate -> Maybe (List (Name, RawImp))    valid (Valid lhs' ups) = Just ups    valid _ = Nothing     fixNames : RawImp -> RawImp    fixNames (IVar loc' (UN n)) = IBindVar loc' n    fixNames (IVar loc' (MN _ _)) = Implicit loc' True    fixNames (IApp loc' f a) = IApp loc' (fixNames f) (fixNames a)    fixNames (IImplicitApp loc' f t a) = IImplicitApp loc' (fixNames f) t (fixNames a)    fixNames tm = tm     updateLHS : List (Name, RawImp) -> RawImp -> RawImp    updateLHS ups (IVar loc' n)        = case lookup n ups of               Nothing => IVar loc' n               Just tm => fixNames tm    updateLHS ups (IBindVar loc' n)        = case lookup (UN n) ups of               Nothing => IBindVar loc' n               Just tm => fixNames tm    updateLHS ups (IApp loc' f a) = IApp loc' (updateLHS ups f) (updateLHS ups a)    updateLHS ups (IImplicitApp loc' f t a)        = IImplicitApp loc' (updateLHS ups f) t (updateLHS ups a)    updateLHS ups tm = tm generateSplits : {auto m : Ref MD Metadata} ->                 {auto c : Ref Ctxt Defs} ->                 {auto u : Ref UST UState} ->                 FC -> Int -> ImpClause ->                 Core (List (Name, List ImpClause))generateSplits loc fn (ImpossibleClause fc lhs) = pure []generateSplits loc fn (WithClause fc lhs wval cs) = pure []generateSplits {c} {m} {u} loc fn (PatClause fc lhs rhs)    = do (lhstm, _) <-                elabTerm fn (InLHS linear) [] (MkNested []) []                         (IBindHere loc PATTERN lhs) Nothing         traverse (trySplit fc lhs lhstm rhs) (splittableNames lhs) mutual  tryAllSplits : {auto c : Ref Ctxt Defs} ->                 {auto m : Ref MD Metadata} ->                 {auto u : Ref UST UState} ->                 FC -> Int -> Error ->                 List (Name, List ImpClause) ->                 Core (List ImpClause)  tryAllSplits loc n err [] = throw err  tryAllSplits loc n err ((x, []) :: rest)      = tryAllSplits loc n err rest  tryAllSplits loc n err ((x, cs) :: rest)      = do log 5 $ "Splitting on " ++ show x           catch (do cs' <- traverse (mkSplits loc n) cs                     pure (concat cs'))                 (\err => tryAllSplits loc n err rest)   mkSplits : {auto c : Ref Ctxt Defs} ->             {auto m : Ref MD Metadata} ->             {auto u : Ref UST UState} ->             FC -> Int -> ImpClause ->             Core (List ImpClause)  -- If the clause works, use it. Otherwise, split on one of the splittable  -- variables and try all of the resulting clauses  mkSplits loc n c      = catch (expandClause loc n c)          (\err =>              do cs <- generateSplits loc n c                 log 5 $ "Splits: " ++ show cs                 tryAllSplits loc n err cs) exportmakeDef : {auto c : Ref Ctxt Defs} ->          {auto m : Ref MD Metadata} ->          {auto u : Ref UST UState} ->          (FC -> (Name, Nat, ClosedTerm) -> Bool) ->          Name -> Core (Maybe (FC, List ImpClause))makeDef p n    = do Just (loc, nidx, envlen, ty) <- findTyDeclAt p            | Nothing => pure Nothing         n <- getFullName nidx         logTerm 5 ("Searching for " ++ show n) ty         defs <- branch         meta <- get MD         ust <- get UST         argns <- getEnvArgNames defs envlen !(nf defs [] ty)         -- Need to add implicit patterns for the outer environment.         -- We won't try splitting on these         let pre_env = replicate envlen (Implicit loc True)          rhshole <- uniqueName defs [] (fnName False n ++ "_rhs")         let initcs = PatClause loc                            (apply (IVar loc n) (pre_env ++ (map (IBindVar loc) argns)))                            (IHole loc rhshole)         let Just nidx = getNameID n (gamma defs)             | Nothing => throw (UndefinedName loc n)         cs' <- mkSplits loc nidx initcs         -- restore the global state, given that we've fiddled with it a lot!         put Ctxt defs         put MD meta         put UST ust         pure (Just (loc, cs'))