0 | module TTImp.Elab.Lazy
  1 |
  2 | import Core.Env
  3 | import Core.Metadata
  4 | import Core.Unify
  5 | import Core.Value
  6 |
  7 | import Idris.REPL.Opts
  8 | import Idris.Syntax
  9 |
 10 | import TTImp.Elab.Check
 11 | import TTImp.Elab.Delayed
 12 | import TTImp.TTImp
 13 |
 14 | %default covering
 15 |
 16 | export
 17 | checkDelayed : {vars : _} ->
 18 |                {auto c : Ref Ctxt Defs} ->
 19 |                {auto m : Ref MD Metadata} ->
 20 |                {auto u : Ref UST UState} ->
 21 |                {auto e : Ref EST (EState vars)} ->
 22 |                {auto s : Ref Syn SyntaxInfo} ->
 23 |                {auto o : Ref ROpts REPLOpts} ->
 24 |                RigCount -> ElabInfo ->
 25 |                NestedNames vars -> Env Term vars ->
 26 |                FC -> LazyReason -> RawImp -> Maybe (Glued vars) ->
 27 |                Core (Term vars, Glued vars)
 28 | checkDelayed rig elabinfo nest env fc r tm exp
 29 |     = do u <- uniVar fc
 30 |          (tm', gty) <- check rig elabinfo nest env tm (Just (gType fc u))
 31 |          pure (TDelayed fc r tm', gty)
 32 |
 33 | export
 34 | checkDelay : {vars : _} ->
 35 |              {auto c : Ref Ctxt Defs} ->
 36 |              {auto m : Ref MD Metadata} ->
 37 |              {auto u : Ref UST UState} ->
 38 |              {auto e : Ref EST (EState vars)} ->
 39 |              {auto s : Ref Syn SyntaxInfo} ->
 40 |              {auto o : Ref ROpts REPLOpts} ->
 41 |              RigCount -> ElabInfo ->
 42 |              NestedNames vars -> Env Term vars ->
 43 |              FC -> RawImp -> Maybe (Glued vars) ->
 44 |              Core (Term vars, Glued vars)
 45 | checkDelay rig elabinfo nest env fc tm mexpected
 46 |     = do expected <- maybe (do nm <- genName "delayTy"
 47 |                                u <- uniVar fc
 48 |                                ty <- metaVar fc erased env nm (TType fc u)
 49 |                                pure (gnf env ty))
 50 |                            pure mexpected
 51 |          let solvemode = case elabMode elabinfo of
 52 |                               InLHS c => inLHS
 53 |                               _ => inTerm
 54 |          solveConstraints solvemode Normal
 55 |          -- Can only check if we know the expected type already because we
 56 |          -- need to infer the delay reason
 57 |          delayOnFailure fc rig env (Just expected) delayError LazyDelay
 58 |             (\delayed =>
 59 |                  case !(getNF expected) of
 60 |                       NDelayed _ r expnf =>
 61 |                          do defs <- get Ctxt
 62 |                             (tm', gty) <- check rig elabinfo nest env tm
 63 |                                                 (Just (glueBack defs env expnf))
 64 |                             tynf <- getNF gty
 65 |                             ty <- getTerm gty
 66 |                             pure (TDelay fc r ty tm',
 67 |                                   glueBack defs env (NDelayed fc r tynf))
 68 |                       ty => do logNF "elab.delay" 5 "Expected delay type" env ty
 69 |                                throw (GenericMsg fc ("Can't infer delay type")))
 70 |   where
 71 |     delayError : Error -> Bool
 72 |     delayError (GenericMsg {}) = True
 73 |     delayError _ = False
 74 |
 75 | export
 76 | checkForce : {vars : _} ->
 77 |              {auto c : Ref Ctxt Defs} ->
 78 |              {auto m : Ref MD Metadata} ->
 79 |              {auto u : Ref UST UState} ->
 80 |              {auto e : Ref EST (EState vars)} ->
 81 |              {auto s : Ref Syn SyntaxInfo} ->
 82 |              {auto o : Ref ROpts REPLOpts} ->
 83 |              RigCount -> ElabInfo ->
 84 |              NestedNames vars -> Env Term vars ->
 85 |              FC -> RawImp -> Maybe (Glued vars) ->
 86 |              Core (Term vars, Glued vars)
 87 | checkForce rig elabinfo nest env fc tm exp
 88 |     = do defs <- get Ctxt
 89 |          expf <- maybe (pure Nothing)
 90 |                        (\gty => do tynf <- getNF gty
 91 |                                    pure (Just (glueBack defs env
 92 |                                          (NDelayed fc LUnknown tynf))))
 93 |                        exp
 94 |          (tm', gty) <- check rig elabinfo nest env tm expf
 95 |          tynf <- getNF gty
 96 |          case tynf of
 97 |               NDelayed _ r expnf =>
 98 |                  pure (TForce fc r tm', glueBack defs env expnf)
 99 |               _ => throw (GenericMsg fc "Forcing a non-delayed type")
100 |