0 | module TTImp.ProcessType
  1 |
  2 | import Core.Env
  3 | import Core.Hash
  4 | import Core.Metadata
  5 | import Core.UnifyState
  6 | import Core.Value
  7 |
  8 | import Idris.REPL.Opts
  9 | import Idris.Syntax
 10 |
 11 | import TTImp.Elab.Check
 12 | import TTImp.Elab.Utils
 13 | import TTImp.Elab
 14 | import TTImp.ProcessFnOpt
 15 | import TTImp.TTImp
 16 |
 17 | import Data.String
 18 | import Libraries.Data.NameMap
 19 | import Libraries.Data.NatSet
 20 | import Libraries.Data.StringMap
 21 | import Libraries.Data.WithDefault
 22 |
 23 | %default covering
 24 | export
 25 | getFnString : {auto c : Ref Ctxt Defs} ->
 26 |               {auto m : Ref MD Metadata} ->
 27 |               {auto u : Ref UST UState} ->
 28 |               {auto s : Ref Syn SyntaxInfo} ->
 29 |               {auto o : Ref ROpts REPLOpts} ->
 30 |                RawImp -> Core String
 31 | getFnString (IPrimVal _ (Str st)) = pure st
 32 | getFnString tm
 33 |     = do inidx <- resolveName (UN $ Basic "[foreign]")
 34 |          let fc = getFC tm
 35 |          let gstr = gnf Env.empty (PrimVal fc $ PrT StringType)
 36 |          etm <- checkTerm inidx InExpr [] (MkNested []) Env.empty tm gstr
 37 |          defs <- get Ctxt
 38 |          case !(nf defs Env.empty etm) of
 39 |               NPrimVal fc (Str st) => pure st
 40 |               _ => throw (GenericMsg fc "%foreign calling convention must evaluate to a String")
 41 |
 42 | -- If it's declared as externally defined, set the definition to
 43 | -- ExternFn <arity>, where the arity is assumed to be fixed (i.e.
 44 | -- not dependent on any of the arguments)
 45 | -- Similarly set foreign definitions. Possibly combine these?
 46 | initDef : {vars : _} ->
 47 |           {auto c : Ref Ctxt Defs} ->
 48 |           {auto m : Ref MD Metadata} ->
 49 |           {auto u : Ref UST UState} ->
 50 |           {auto s : Ref Syn SyntaxInfo} ->
 51 |           {auto o : Ref ROpts REPLOpts} ->
 52 |           FC -> Name -> Env Term vars -> Term vars -> List FnOpt -> Core Def
 53 | initDef fc n env ty []
 54 |     = do addUserHole False n
 55 |          pure None
 56 | initDef fc n env ty (ExternFn :: opts)
 57 |     = do defs <- get Ctxt
 58 |          a <- getArity defs env ty
 59 |          pure (ExternDef a)
 60 | initDef fc n env ty (ForeignFn cs :: opts)
 61 |     = do defs <- get Ctxt
 62 |          a <- getArity defs env ty
 63 |          cs' <- traverse getFnString cs
 64 |          pure (ForeignDef a cs')
 65 | -- In this case, nothing to initialise to, but we do need to process the
 66 | -- calling conventions then process the rest of the options.
 67 | -- This means, for example, we can technically re-export something foreign!
 68 | -- I suppose that may be useful one day...
 69 | initDef fc n env ty (ForeignExport cs :: opts)
 70 |     = do cs' <- traverse getFnString cs
 71 |          conv <- traverse getConvention cs'
 72 |          defs <- get Ctxt
 73 |          put Ctxt ({ foreignExports $= insert n conv } defs)
 74 |          initDef fc n env ty opts
 75 |   where
 76 |     getConvention : String -> Core (String, String)
 77 |     getConvention c
 78 |         = do let (lang ::: fname :: []) = split (== ':') c
 79 |                  | _ => throw (GenericMsg fc "Invalid calling convention")
 80 |              pure (trim lang, trim fname)
 81 | initDef fc n env ty (_ :: opts) = initDef fc n env ty opts
 82 |
 83 | -- Find the inferrable argument positions in a type. This is useful for
 84 | -- generalising partially evaluated definitions and (potentially) in interactive
 85 | -- editing
 86 | findInferrable : {auto c : Ref Ctxt Defs} ->
 87 |                  Defs -> ClosedNF -> Core NatSet
 88 | findInferrable defs ty = fi 0 0 [] NatSet.empty ty
 89 |   where
 90 |     mutual
 91 |       -- Add to the inferrable arguments from the given type. An argument is
 92 |       -- inferrable if it's guarded by a constructor, or on its own
 93 |       findInf : NatSet -> List (Name, Nat) ->
 94 |                 ClosedNF -> Core NatSet
 95 |       findInf acc pos (NApp _ (NRef Bound n) [])
 96 |           = case lookup n pos of
 97 |                  Nothing => pure acc
 98 |                  Just p => if p `elem` acc then pure acc else pure (NatSet.insert p acc)
 99 |       findInf acc pos (NDCon _ _ _ _ args)
100 |           = do args' <- traverse (evalClosure defs . snd) args
101 |                findInfs acc pos args'
102 |       findInf acc pos (NTCon _ _ _ args)
103 |           = do args' <- traverse (evalClosure defs . snd) args
104 |                findInfs acc pos args'
105 |       findInf acc pos (NDelayed _ _ t) = findInf acc pos t
106 |       findInf acc _ _ = pure acc
107 |
108 |       findInfs : NatSet -> List (Name, Nat) -> List ClosedNF -> Core NatSet
109 |       findInfs acc pos [] = pure acc
110 |       findInfs acc pos (n :: ns) = findInf !(findInfs acc pos ns) pos n
111 |
112 |     fi : Nat -> Int -> List (Name, Nat) -> NatSet -> ClosedNF -> Core NatSet
113 |     fi pos i args acc (NBind fc x (Pi _ _ _ aty) sc)
114 |         = do let argn = MN "inf" i
115 |              sc' <- sc defs (toClosure defaultOpts Env.empty (Ref fc Bound argn))
116 |              acc' <- findInf acc args !(evalClosure defs aty)
117 |              rest <- fi (1 + pos) (1 + i) ((argn, pos) :: args) acc' sc'
118 |              pure rest
119 |     fi pos i args acc ret = findInf acc args ret
120 |
121 | checkForShadowing : (env : StringMap FC) -> RawImp -> StringMap (FC, FC)
122 | checkForShadowing env (IPi fc _ _ nm argTy retTy)
123 |     = do let argShadowing = checkForShadowing empty argTy
124 |          let retShadowing =
125 |             case nm of
126 |               (Just (UN (Basic name))) =>
127 |                 case lookup name env of
128 |                   Just origFc => insert name (origFc, fc) $ checkForShadowing env retTy
129 |                   Nothing => checkForShadowing (insert name fc env) retTy
130 |               _ => checkForShadowing env retTy
131 |          argShadowing `mergeLeft` retShadowing
132 | checkForShadowing env _ = empty
133 |
134 | export
135 | processType : {vars : _} ->
136 |               {auto c : Ref Ctxt Defs} ->
137 |               {auto m : Ref MD Metadata} ->
138 |               {auto u : Ref UST UState} ->
139 |               {auto s : Ref Syn SyntaxInfo} ->
140 |               {auto o : Ref ROpts REPLOpts} ->
141 |               List ElabOpt -> NestedNames vars -> Env Term vars ->
142 |               FC -> RigCount -> Visibility ->
143 |               List FnOpt -> ImpTy -> Core ()
144 | processType {vars} eopts nest env fc rig vis opts ty_raw
145 |     = do let typeName = ty_raw.tyName
146 |          n <- inCurrentNS typeName.val
147 |          let tfc = ty_raw.fc
148 |
149 |          addNameLoc typeName.fc n
150 |
151 |          log "declare.type" 1 $ "Processing " ++ show n
152 |          log "declare.type" 5 $ unwords ["Checking type decl:", show rig, show n, ":", show ty_raw]
153 |          idx <- resolveName n
154 |
155 |          -- Check 'n' is undefined
156 |          defs <- get Ctxt
157 |          Nothing <- lookupCtxtExact (Resolved idx) (gamma defs)
158 |               | Just gdef => throw (AlreadyDefined fc n)
159 |
160 |          u <- uniVar fc
161 |          ty <-
162 |              wrapErrorC eopts (InType fc n) $
163 |                    checkTerm idx InType (HolesOkay :: eopts) nest env
164 |                              (IBindHere fc (PI erased) ty_raw.val)
165 |                              (gType fc u)
166 |          logTermNF "declare.type" 3 ("Type of " ++ show n) Env.empty (abstractFullEnvType tfc env ty)
167 |
168 |          def <- initDef fc n env ty opts
169 |          let fullty = abstractFullEnvType tfc env ty
170 |
171 |          (erased, dterased) <- findErased fullty
172 |          defs <- get Ctxt
173 |          empty <- clearDefs defs
174 |          infargs <- findInferrable empty !(nf defs Env.empty fullty)
175 |
176 |          ignore $ addDef (Resolved idx)
177 |                 ({ eraseArgs := erased,
178 |                    safeErase := dterased,
179 |                    inferrable := infargs }
180 |                  (newDef fc n rig vars fullty (specified vis) def))
181 |          -- Flag it as checked, because we're going to check the clauses
182 |          -- from the top level.
183 |          -- But, if it's a case block, it'll be checked as part of the top
184 |          -- level check so don't set the flag.
185 |          unless (InCase `elem` eopts) $ setLinearCheck idx True
186 |
187 |          log "declare.type" 2 $ "Setting options for " ++ show n ++ ": " ++ show opts
188 |          let name = Resolved idx
189 |          let isNested : Name -> Bool
190 |              isNested (Nested {}) = True
191 |              isNested (NS _ n) = isNested n
192 |              isNested _ = False
193 |          let nested = not (isNested n)
194 |          traverse_ (processFnOpt fc (not (isNested n)) name) opts
195 |          -- If no function-specific totality pragma has been used, attach the default totality
196 |          unless (any isTotalityReq opts) $
197 |            setFlag fc name (SetTotal !getDefaultTotalityOption)
198 |
199 |          -- Add to the interactive editing metadata
200 |          addTyDecl fc (Resolved idx) env ty -- for definition generation
201 |
202 |          log "metadata.names" 7 $ "processType is adding ↓"
203 |          addNameType typeName.fc (Resolved idx) env ty -- for looking up types
204 |
205 |          traverse_ addToSave (keys (getMetas ty))
206 |          addToSave n
207 |          log "declare.type" 10 $ "Saving from " ++ show n ++ ": " ++ show (keys (getMetas ty))
208 |
209 |          when (vis /= Private) $
210 |               do addHashWithNames n
211 |                  addHashWithNames ty
212 |                  log "module.hash" 15 "Adding hash for type with name \{show n}"
213 |
214 |          when (showShadowingWarning !getSession) $
215 |             whenJust (fromList $ toList $ checkForShadowing StringMap.empty ty_raw.val)
216 |                 $ recordWarning . ShadowingLocalBindings fc
217 |