module TTImp.ProcessParams import Core.Contextimport Core.Envimport Core.TTimport Core.Unifyimport Core.Metadataimport Core.Normalise import TTImp.BindImplicitsimport TTImp.Elabimport TTImp.Elab.Checkimport TTImp.TTImp %default covering extend : Env Term extvs -> SubVars vs extvs ->         NestedNames extvs ->         Term extvs ->         (vars' ** (SubVars vs vars', Env Term vars', NestedNames vars'))extend env p nest (Bind fc n (Pi c e ty) sc)    = extend (Pi c e ty :: env) (DropCons p) (weaken nest) scextend env p nest tm = (_ ** (p, env, nest)) exportprocessParams : {vars : _} ->                {auto c : Ref Ctxt Defs} ->                {auto m : Ref MD Metadata} ->                {auto u : Ref UST UState} ->                NestedNames vars ->                Env Term vars ->                FC -> List (Name, RawImp) -> List ImpDecl ->                Core ()processParams {vars} {c} {m} {u} nest env fc ps ds    = do -- Turn the parameters into a function type, (x : ps) -> Type,         -- then read off the environment from the elaborated type. This way         -- we'll get all the implicit names we need         let pty_raw = mkParamTy ps         pty_imp <- bindTypeNames [] vars (IBindHere fc (PI Rig0) pty_raw)         log 10 $ "Checking " ++ show pty_imp         pty <- checkTerm (-1) InType []                          nest env pty_imp (gType fc)         let (vs ** (prf, env', nest')) = extend env SubRefl nest pty          -- Treat the names in the block as 'nested names' so that we expand         -- the applications as we need to         defs <- get Ctxt         let defNames = definedInBlock (currentNS defs) ds         names' <- traverse (applyEnv env') defNames         let nestBlock = record { names $= (names' ++) } nest'         traverse (processDecl [] nestBlock env') ds         pure ()  where    mkParamTy : List (Name, RawImp) -> RawImp    mkParamTy [] = IType fc    mkParamTy ((n, ty) :: ps)       = IPi fc RigW Explicit (Just n) ty (mkParamTy ps)     applyEnv : Env Term vs -> Name ->               Core (Name, (Maybe Name, List Name, FC -> NameType -> Term vs))    applyEnv env n          = do n' <- resolveName n -- it'll be Resolved by expandAmbigName               pure (Resolved n', (Nothing, namesNoLet env,                        \fc, nt => applyTo fc                               (Ref fc nt (Resolved n')) env))