module Idris.Elab.Implementation import Core.Binaryimport Core.Contextimport Core.Coreimport Core.Envimport Core.Metadataimport Core.TTimport Core.Unify import Idris.Resugarimport Idris.Syntax import TTImp.BindImplicitsimport TTImp.Elabimport TTImp.Elab.Checkimport TTImp.ProcessDeclsimport TTImp.TTImpimport TTImp.Unelabimport TTImp.Utils import Control.Monad.Stateimport Data.ANameMapimport Data.NameMap %default covering mkImpl : FC -> Name -> List RawImp -> NamemkImpl fc n ps    = DN (show n ++ " implementation at " ++ show fc)         (UN ("__Impl_" ++ show n ++ "_" ++          showSep "_" (map show ps))) bindConstraints : FC -> PiInfo RawImp ->                  List (Maybe Name, RawImp) -> RawImp -> RawImpbindConstraints fc p [] ty = tybindConstraints fc p ((n, ty) :: rest) sc    = IPi fc RigW p n ty (bindConstraints fc p rest sc) bindImpls : FC -> List (Name, RigCount, RawImp) -> RawImp -> RawImpbindImpls fc [] ty = tybindImpls fc ((n, r, ty) :: rest) sc    = IPi fc r Implicit (Just n) ty (bindImpls fc rest sc) addDefaults : FC -> Name -> List Name -> List (Name, List ImpClause) ->              List ImpDecl ->              (List ImpDecl, List Name) -- Updated body, list of missing methodsaddDefaults fc impName allms defs body    = let missing = dropGot allms body in          extendBody [] missing body  where    -- Given the list of missing names, if any are among the default definitions,    -- add them to the body    extendBody : List Name -> List Name -> List ImpDecl ->                 (List ImpDecl, List Name)    extendBody ms [] body = (body, ms)    extendBody ms (n :: ns) body        = case lookup n defs of               Nothing => extendBody (n :: ms) ns body               Just cs =>                    -- If any method names appear in the clauses, they should                    -- be applied to the constraint name __con because they                    -- are going to be referring to the present implementation.                    -- That is, default method implementations could depend on                    -- other methods.                    -- (See test idris2/interface014 for an example!)                    let mupdates                            = map (\n => (n, IImplicitApp fc (IVar fc n)                                                          (Just (UN "__con"))                                                          (IVar fc impName))) allms                        cs' = map (substNamesClause [] mupdates) cs in                        extendBody ms ns                             (IDef fc n (map (substLocClause fc) cs') :: body)     -- Find which names are missing from the body    dropGot : List Name -> List ImpDecl -> List Name    dropGot ms [] = ms    dropGot ms (IDef _ n _ :: ds)        = dropGot (filter (/= n) ms) ds    dropGot ms (_ :: ds) = dropGot ms ds getMethImps : {auto c : Ref Ctxt Defs} ->              Env Term vars -> Term vars ->              Core (List (Name, RigCount, RawImp))getMethImps env (Bind fc x (Pi c Implicit ty) sc)    = do rty <- unelabNoSugar env ty         ts <- getMethImps (Pi c Implicit ty :: env) sc         pure ((x, c, rty) :: ts)getMethImps env tm = pure [] exportelabImplementation : {auto c : Ref Ctxt Defs} ->                     {auto u : Ref UST UState} ->                     {auto s : Ref Syn SyntaxInfo} ->                     {auto m : Ref MD Metadata} ->                     FC -> Visibility -> List FnOpt -> Pass ->                     Env Term vars -> NestedNames vars ->                     (implicits : List (Name, RigCount, RawImp)) ->                     (constraints : List (Maybe Name, RawImp)) ->                     Name ->                     (ps : List RawImp) ->                     (implName : Maybe Name) ->                     (nusing : List Name) ->                     Maybe (List ImpDecl) ->                     Core ()-- TODO: Refactor all these steps into separate functionselabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nusing mbody    = do let impName_in = maybe (mkImpl fc iname ps) id impln         impName <- inCurrentNS impName_in         syn <- get Syn         let [cndata] = lookupName iname (ifaces syn)             | [] => throw (UndefinedName fc iname)             | ns => throw (AmbiguousName fc (map fst ns))         let cn : Name = fst cndata         let cdata : IFaceInfo = snd cndata         defs <- get Ctxt          Just ity <- lookupTyExact cn (gamma defs)              | Nothing => throw (UndefinedName fc cn)         Just conty <- lookupTyExact (iconstructor cdata) (gamma defs)              | Nothing => throw (UndefinedName fc (iconstructor cdata))          let impsp = nub (concatMap findIBinds ps ++                          concatMap findIBinds (map snd cons))          logTerm 3 ("Found interface " ++ show cn) ity         log 3 $ " with params: " ++ show (params cdata)                 ++ " and parents: " ++ show (parents cdata)                 ++ " using implicits: " ++ show impsp                 ++ " and methods: " ++ show (methods cdata) ++ "\n"                 ++ "Constructor: " ++ show (iconstructor cdata) ++ "\n"         logTerm 3 "Constructor type: " conty         log 5 $ "Making implementation " ++ show impName          -- 1. Build the type for the implementation         -- Make the constraints auto implicit arguments, which can be explicitly         -- given when using named implementations         --    (cs : Constraints) -> Impl params         -- Don't make it a hint if it's a named implementation         let opts = maybe (opts_in ++ [Inline, Hint True])                          (const (opts_in ++ [Inline])) impln          let initTy = bindImpls fc is $ bindConstraints fc AutoImplicit cons                         (apply (IVar fc iname) ps)         let paramBinds = if !isUnboundImplicits                          then findBindableNames True vars [] initTy                          else []         let impTy = doBind paramBinds initTy          let impTyDecl = IClaim fc RigW vis opts (MkImpTy fc impName impTy)         log 5 $ "Implementation type: " ++ show impTy          when (typePass pass) $ processDecl [] nest env impTyDecl          -- If the body is empty, we're done for now (just declaring that         -- the implementation exists and define it later)         when (defPass pass) $ maybe (pure ())           (\body_in => do               defs <- get Ctxt               Just impTyc <- lookupTyExact impName (gamma defs)                    | Nothing => throw (InternalError ("Can't happen, can't find type of " ++ show impName))               methImps <- getMethImps [] impTyc               log 3 $ "Bind implicits to each method: " ++ show methImps                -- 1.5. Lookup default definitions and add them to to body               let (body, missing)                     = addDefaults fc impName (map (dropNS . fst) (methods cdata))                                      (defaults cdata) body_in                log 5 $ "Added defaults: body is " ++ show body               log 5 $ "Missing methods: " ++ show missing                -- Add the 'using' hints               log 10 $ "Open hints: " ++ (show (impName :: nusing))               traverse_ (\n => do n' <- checkUnambig fc n                                   addOpenHint n') nusing                -- 2. Elaborate top level function types for this interface               defs <- get Ctxt               fns <- topMethTypes [] impName methImps impsp (params cdata)                                      (map fst (methods cdata))                                      (methods cdata)               traverse (processDecl [] nest env) (map mkTopMethDecl fns)                -- 3. Build the record for the implementation               let mtops = map (Basics.fst . snd) fns               let con = iconstructor cdata               let ilhs = impsApply (IVar fc impName)                                    (map (\x => (x, IBindVar fc (show x)))                                              (map fst methImps))               -- RHS is the constructor applied to a search for the necessary               -- parent constraints, then the method implementations               defs <- get Ctxt               let fldTys = getFieldArgs !(normaliseHoles defs [] conty)               log 5 $ "Field types " ++ show fldTys               let irhs = apply (IVar fc con)                                (map (const (ISearch fc 500)) (parents cdata)                                 ++ map (mkMethField methImps fldTys) fns)               let impFn = IDef fc impName [PatClause fc ilhs irhs]               log 5 $ "Implementation record: " ++ show impFn                -- If it's a named implementation, add it as a global hint while               -- elaborating the record and bodies               defs <- get Ctxt               let hs = openHints defs               maybe (pure ()) (\x => addOpenHint impName) impln                -- Make sure we don't use this name to solve parent constraints               -- when elaborating the record, or we'll end up in a cycle!               setFlag fc impName BlockedHint               traverse (processDecl [] nest env) [impFn]               unsetFlag fc impName BlockedHint                setFlag fc impName TCInline                -- 4. (TODO: Order method bodies to be in declaration order, in               --    case of dependencies)                -- 5. Elaborate the method bodies                body' <- traverse (updateBody (map methNameUpdate fns)) body               log 10 $ "Implementation body: " ++ show body'               traverse (processDecl [] nest env) body'               -- Reset the open hints (remove the named implementation)               setOpenHints hs               pure ()) mbody  where    -- For the method fields in the record, get the arguments we need to abstract    -- over    getFieldArgs : Term vs -> List (Name, List (Name, RigCount, PiInfo RawImp))    getFieldArgs (Bind _ x (Pi c p ty) sc)        = (x, getArgs ty) :: getFieldArgs sc      where        getArgs : Term vs' -> List (Name, RigCount, PiInfo RawImp)        getArgs (Bind _ x (Pi c p _) sc)            = (x, c, forgetDef p) :: getArgs sc        getArgs _ = []    getFieldArgs _ = []     impsApply : RawImp -> List (Name, RawImp) -> RawImp    impsApply fn [] = fn    impsApply fn ((n, arg) :: ns)        = impsApply (IImplicitApp fc fn (Just n) arg) ns     mkLam : List (Name, RigCount, PiInfo RawImp) -> RawImp -> RawImp    mkLam [] tm = tm    mkLam ((x, c, p) :: xs) tm        = ILam fc c p (Just x) (Implicit fc False) (mkLam xs tm)     applyTo : FC -> RawImp -> List (Name, RigCount, PiInfo RawImp) -> RawImp    applyTo fc tm [] = tm    applyTo fc tm ((x, c, Explicit) :: xs)        = applyTo fc (IApp fc tm (IVar fc x)) xs    applyTo fc tm ((x, c, AutoImplicit) :: xs)        = applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs    applyTo fc tm ((x, c, Implicit) :: xs)        = applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs    applyTo fc tm ((x, c, DefImplicit _) :: xs)        = applyTo fc (IImplicitApp fc tm (Just x) (IVar fc x)) xs     -- When applying the method in the field for the record, eta expand    -- the expected arguments based on the field type, so that implicits get    -- inserted in the right place    mkMethField : List (Name, RigCount, RawImp) ->                  List (Name, List (Name, RigCount, PiInfo RawImp)) ->                  (Name, Name, List (String, String), RigCount, RawImp) -> RawImp    mkMethField methImps fldTys (topn, n, upds, c, ty)        = let argns = map applyUpdate (maybe [] id (lookup (dropNS topn) fldTys))              imps = map fst methImps in              -- Pass through implicit arguments to the function which are also              -- implicit arguments to the declaration              mkLam argns                    (impsApply                         (applyTo fc (IVar fc n) argns)                         (map (\n => (n, IVar fc (UN (show n)))) imps))      where        applyUpdate : (Name, RigCount, PiInfo RawImp) ->                      (Name, RigCount, PiInfo RawImp)        applyUpdate (UN n, c, p)            = maybe (UN n, c, p) (\n' => (UN n', c, p)) (lookup n upds)        applyUpdate t = t     methName : Name -> Name    methName (NS _ n) = methName n    methName n        = DN (show n) (UN (show n ++ "_" ++ show iname ++ "_" ++                     maybe "" show impln ++ "_" ++                     showSep "_" (map show ps)))     applyCon : Name -> Name -> Core (Name, RawImp)    applyCon impl n        = do mn <- inCurrentNS (methName n)             pure (dropNS n, IVar fc mn)     bindImps : List (Name, RigCount, RawImp) -> RawImp -> RawImp    bindImps [] ty = ty    bindImps ((n, c, t) :: ts) ty        = IPi fc c Implicit (Just n) t (bindImps ts ty)     -- Return method name, specialised method name, implicit name updates,    -- and method type. Also return how the method name should be updated    -- in later method types (specifically, putting implicits in)    topMethType : List (Name, RawImp) ->                  Name -> List (Name, RigCount, RawImp) ->                  List String -> List Name -> List Name ->                  (Name, RigCount, (Bool, RawImp)) ->                  Core ((Name, Name, List (String, String), RigCount, RawImp),                           List (Name, RawImp))    topMethType methupds impName methImps impsp pnames allmeths (mn, c, (d, mty_in))        = do -- Get the specialised type by applying the method to the             -- parameters             n <- inCurrentNS (methName mn)              -- Avoid any name clashes between parameters and method types by             -- renaming IBindVars in the method types which appear in the             -- parameters             let upds' = !(traverse (applyCon impName) allmeths)             let mty_in = substNames vars upds' mty_in             let (mty_in, upds) = runState (renameIBinds impsp (findImplicits mty_in) mty_in) []             -- Finally update the method type so that implicits from the             -- parameters are passed through to any earlier methods which             -- appear in the type             let mty_in = substNames vars methupds mty_in             let mbase = bindImps methImps $                         bindConstraints fc AutoImplicit cons $                         substNames vars (zip pnames ps) mty_in             let ibound = findImplicits mbase              mty <- bindTypeNamesUsed ibound vars mbase              log 3 $ "Method " ++ show mn ++ " ==> " ++                     show n ++ " : " ++ show mty             log 3 $ "    (initially " ++ show mty_in ++ ")"             log 5 $ "Updates " ++ show methupds             log 5 $ "From " ++ show mbase             log 3 $ "Name updates " ++ show upds             log 3 $ "Param names: " ++ show pnames             log 10 $ "Used names " ++ show ibound             let ibinds = map fst methImps             let methupds' = if isNil ibinds then []                             else [(n, impsApply (IVar fc n)                                     (map (\x => (x, IBindVar fc (show x))) ibinds))]             pure ((mn, n, upds, c, mty), methupds')     topMethTypes : List (Name, RawImp) ->                   Name -> List (Name, RigCount, RawImp) ->                   List String -> List Name -> List Name ->                   List (Name, RigCount, (Bool, RawImp)) ->                   Core (List (Name, Name, List (String, String), RigCount, RawImp))    topMethTypes upds impName methImps impsp pnames allmeths [] = pure []    topMethTypes upds impName methImps impsp pnames allmeths (m :: ms)        = do (m', newupds) <- topMethType upds impName methImps impsp pnames allmeths m             ms' <- topMethTypes (newupds ++ upds) impName methImps impsp pnames allmeths ms             pure (m' :: ms')     mkTopMethDecl : (Name, Name, List (String, String), RigCount, RawImp) -> ImpDecl    mkTopMethDecl (mn, n, upds, c, mty)        = IClaim fc c vis opts_in (MkImpTy fc n mty)     -- Given the method type (result of topMethType) return the mapping from    -- top level method name to current implementation's method name    methNameUpdate : (Name, Name, t) -> (Name, Name)    methNameUpdate (mn, fn, _) = (UN (nameRoot mn), fn)     findMethName : List (Name, Name) -> FC -> Name -> Core Name    findMethName ns fc n        = case lookup n ns of               Nothing => throw (GenericMsg fc                                (show n ++ " is not a method of " ++                                 show iname))               Just n' => pure n'     updateApp : List (Name, Name) -> RawImp -> Core RawImp    updateApp ns (IVar fc n)        = do n' <- findMethName ns fc n             pure (IVar fc n')    updateApp ns (IApp fc f arg)        = do f' <- updateApp ns f             pure (IApp fc f' arg)    updateApp ns (IImplicitApp fc f x arg)        = do f' <- updateApp ns f             pure (IImplicitApp fc f' x arg)    updateApp ns tm        = throw (GenericMsg (getFC tm) "Invalid method definition")     updateClause : List (Name, Name) -> ImpClause ->                   Core ImpClause    updateClause ns (PatClause fc lhs rhs)        = do lhs' <- updateApp ns lhs             pure (PatClause fc lhs' rhs)    updateClause ns (WithClause fc lhs wval cs)        = do lhs' <- updateApp ns lhs             cs' <- traverse (updateClause ns) cs             pure (WithClause fc lhs' wval cs')    updateClause ns (ImpossibleClause fc lhs)        = do lhs' <- updateApp ns lhs             pure (ImpossibleClause fc lhs')     updateBody : List (Name, Name) -> ImpDecl -> Core ImpDecl    updateBody ns (IDef fc n cs)        = do cs' <- traverse (updateClause ns) cs             n' <- findMethName ns fc n             pure (IDef fc n' cs')    updateBody ns _        = throw (GenericMsg fc                   "Implementation body can only contain definitions")