0 | module Core.GetType
  1 |
  2 | import Core.Context
  3 | import Core.Env
  4 | import Core.Normalise
  5 | import Core.Value
  6 |
  7 | %default covering
  8 |
  9 | -- Get the type of an already typechecked thing.
 10 | -- We need this (occasionally) because we don't store types in subterms (e.g. on
 11 | -- applications) and we don't keep the type of suterms up to date throughout
 12 | -- unification. Perhaps we should? There's a trade off here, and recalculating on
 13 | -- the rare occasions it's necessary doesn't seem to cost too much, but keep an
 14 | -- eye on it...
 15 |
 16 | mutual
 17 |   chk : {vars : _} ->
 18 |         {auto c : Ref Ctxt Defs} ->
 19 |         Env Term vars -> Term vars -> Core (Glued vars)
 20 |   chk env (Local fc r idx p)
 21 |       = pure $ gnf env (binderType (getBinder p env))
 22 |   chk env (Ref fc nt n)
 23 |       = do defs <- get Ctxt
 24 |            Just ty <- lookupTyExact n (gamma defs)
 25 |                | Nothing => undefinedName fc n
 26 |            pure $ gnf env (embed ty)
 27 |   chk env (Meta fc n i args)
 28 |       = do defs <- get Ctxt
 29 |            Just mty <- lookupTyExact (Resolved i) (gamma defs)
 30 |                | Nothing => undefinedName fc n
 31 |            chkMeta fc env !(nf defs env (embed mty)) args
 32 |   chk env (Bind fc nm b sc)
 33 |       = do bt <- chkBinder env b
 34 |            sct <- chk {vars = nm :: _} (b :: env) sc
 35 |            pure $ gnf env (discharge fc nm b !(getTerm bt) !(getTerm sct))
 36 |   chk env (App fc f a)
 37 |       = do fty <- chk env f
 38 |            case !(getNF fty) of
 39 |                 NBind _ _ (Pi _ _ _ ty) scdone =>
 40 |                       do defs <- get Ctxt
 41 |                          aty <- chk env a
 42 |                          sc' <- scdone defs (toClosure defaultOpts env a)
 43 |                          pure $ glueBack defs env sc'
 44 |                 _ => do fty' <- getTerm fty
 45 |                         throw (NotFunctionType fc env fty')
 46 |   chk env (As fc s n p) = chk env p
 47 |   chk env (TDelayed fc r tm) = pure (gType fc (MN "top" 0))
 48 |   chk env (TDelay fc r dty tm)
 49 |       = do gtm <- chk env tm
 50 |            tm' <- getNF gtm
 51 |            defs <- get Ctxt
 52 |            pure $ glueBack defs env (NDelayed fc r tm')
 53 |   chk env (TForce fc r tm)
 54 |       = do tm' <- chk env tm
 55 |            case !(getNF tm') of
 56 |                 NDelayed fc _ fty =>
 57 |                     do defs <- get Ctxt
 58 |                        pure $ glueBack defs env fty
 59 |                 _ => throw (GenericMsg fc "Not a delayed type")
 60 |   chk env (PrimVal fc x) = pure $ gnf env (chkConstant fc x)
 61 |   chk env (TType fc u) = pure (gType fc (MN "top" 0))
 62 |   chk env (Erased fc _) = pure (gErased fc)
 63 |
 64 |   chkMeta : {vars : _} ->
 65 |             {auto c : Ref Ctxt Defs} ->
 66 |             FC -> Env Term vars -> NF vars -> List (Term vars) ->
 67 |             Core (Glued vars)
 68 |   chkMeta fc env ty []
 69 |       = do defs <- get Ctxt
 70 |            pure $ glueBack defs env ty
 71 |   chkMeta fc env (NBind _ _ (Pi _ _ _ ty) scdone) (a :: args)
 72 |       = do defs <- get Ctxt
 73 |            aty <- chk env a
 74 |            sc' <- scdone defs (toClosure defaultOpts env a)
 75 |            chkMeta fc env sc' args
 76 |   chkMeta fc env ty args
 77 |       = do defs <- get Ctxt
 78 |            throw (NotFunctionType fc env !(quote defs env ty))
 79 |
 80 |   chkBinder : {vars : _} ->
 81 |               {auto c : Ref Ctxt Defs} ->
 82 |               Env Term vars -> Binder (Term vars) -> Core (Glued vars)
 83 |   chkBinder env b = chk env (binderType b)
 84 |
 85 |   discharge : FC -> (nm : Name) -> Binder (Term vars) ->
 86 |               Term vars -> Term (nm :: vars) -> (Term vars)
 87 |   discharge fc n (Lam fc' c x ty) bindty scopety
 88 |       = Bind fc n (Pi fc' c x ty) scopety
 89 |   discharge fc n (Let fc' c val ty) bindty scopety
 90 |       = Bind fc n (Let fc' c val ty) scopety
 91 |   discharge fc n (Pi {}) bindty scopety
 92 |       = bindty
 93 |   discharge fc n (PVar fc' c p ty) bindty scopety
 94 |       = Bind fc n (PVTy fc' c ty) scopety
 95 |   discharge fc n (PLet fc' c val ty) bindty scopety
 96 |       = Bind fc n (PLet fc' c val ty) scopety
 97 |   discharge fc n (PVTy {}) bindty scopety
 98 |       = bindty
 99 |
100 |   chkConstant : FC -> Constant -> Term vars
101 |   chkConstant fc (I x)    = PrimVal fc $ PrT IntType
102 |   chkConstant fc (I8 x)   = PrimVal fc $ PrT Int8Type
103 |   chkConstant fc (I16 x)  = PrimVal fc $ PrT Int16Type
104 |   chkConstant fc (I32 x)  = PrimVal fc $ PrT Int32Type
105 |   chkConstant fc (I64 x)  = PrimVal fc $ PrT Int64Type
106 |   chkConstant fc (BI x)   = PrimVal fc $ PrT IntegerType
107 |   chkConstant fc (B8 x)   = PrimVal fc $ PrT Bits8Type
108 |   chkConstant fc (B16 x)  = PrimVal fc $ PrT Bits16Type
109 |   chkConstant fc (B32 x)  = PrimVal fc $ PrT Bits32Type
110 |   chkConstant fc (B64 x)  = PrimVal fc $ PrT Bits64Type
111 |   chkConstant fc (Str x)  = PrimVal fc $ PrT StringType
112 |   chkConstant fc (Ch x)   = PrimVal fc $ PrT CharType
113 |   chkConstant fc (Db x)   = PrimVal fc $ PrT DoubleType
114 |   chkConstant fc WorldVal = PrimVal fc $ PrT WorldType
115 |   chkConstant fc _        = TType fc (MN "top" 0)
116 |
117 | export
118 | getType : {vars : _} ->
119 |           {auto c : Ref Ctxt Defs} ->
120 |           Env Term vars -> (term : Term vars) -> Core (Glued vars)
121 | getType env term = chk env term
122 |