
  0 | module TTImp.ProcessParams
  1 | 
  2 | import Core.Env
  3 | import Core.UnifyState
  4 | import Core.Metadata
  5 | 
  6 | import Idris.REPL.Opts
  7 | import Idris.Syntax
  8 | 
  9 | import TTImp.BindImplicits
 10 | import TTImp.Elab
 11 | import TTImp.Elab.Check
 12 | import TTImp.TTImp
 13 | 
 14 | %default covering
 15 | 
 16 | extend : {extvs : _} ->
 17 |          Env Term extvs -> Thin vs extvs ->
 18 |          NestedNames extvs ->
 19 |          Term extvs ->
 20 |          (vars' ** (Thin vs vars', Env Term vars', NestedNames vars'))
 21 | extend env p nest (Bind _ n b@(Pi fc c pi ty) sc)
 22 |     = extend (b :: env) (Drop p) (weaken nest) sc
 23 | extend env p nest tm = (_ ** (p, env, nest))
 24 | 
 25 | export
 26 | processParams : {vars : _} ->
 27 |                 {auto c : Ref Ctxt Defs} ->
 28 |                 {auto m : Ref MD Metadata} ->
 29 |                 {auto u : Ref UST UState} ->
 30 |                 {auto s : Ref Syn SyntaxInfo} ->
 31 |                 {auto o : Ref ROpts REPLOpts} ->
 32 |                 NestedNames vars ->
 33 |                 Env Term vars ->
 34 |                 FC -> List ImpParameter -> List ImpDecl ->
 35 |                 Core ()
 36 | processParams {vars} {c} {m} {u} nest env fc ps ds
 37 |     = do -- Turn the parameters into a function type, (x : ps) -> Type,
 38 |          -- then read off the environment from the elaborated type. This way
 39 |          -- we'll get all the implicit names we need
 40 |          let pty_raw = mkParamTy ps
 41 |          pty_imp <- bindTypeNames fc [] (toList vars) (IBindHere fc (PI erased) pty_raw)
 42 |          log "declare.param" 10 $ "Checking " ++ show pty_imp
 43 |          u <- uniVar fc
 44 |          pty <- checkTerm (-1) InType []
 45 |                           nest env pty_imp (gType fc u)
 46 |          let (vs ** (prf, env', nest')) = extend env Refl nest pty
 47 |          logEnv "declare.param" 5 "Param env" env'
 48 | 
 49 |          -- Treat the names in the block as 'nested names' so that we expand
 50 |          -- the applications as we need to
 51 |          defs <- get Ctxt
 52 |          let defNames = definedInBlock (currentNS defs) ds
 53 |          names' <- traverse (applyEnv env') defNames
 54 |          let nestBlock = { names $= (names' ++) } nest'
 55 |          traverse_ (processDecl [] nestBlock env') ds
 56 |   where
 57 |     mkParamTy : List ImpParameter -> RawImp
 58 |     mkParamTy [] = IType fc
 59 |     mkParamTy (binder :: ps)
 60 |        = IPi fc binder.rig binder.val.info (Just binder.name.val) binder.val.boundType (mkParamTy ps)
 61 | 
 62 |     applyEnv : {vs : _} ->
 63 |                Env Term vs -> Name ->
 64 |                Core (Name, (Maybe Name, List (Var vs), FC -> NameType -> Term vs))
 65 |     applyEnv {vs} env n
 66 |           = do n' <- resolveName n -- it'll be Resolved by expandAmbigName
 67 |                pure (Resolved n', (Nothing, reverse (allVars env),
 68 |                         \fc, nt => applyToFull fc
 69 |                                (Ref fc nt (Resolved n')) env))
 70 |