0 | ||| Checking a %builtin pragma is correct.
  1 | -- If we get more builtins it might be wise to move each builtin to its own file.
  2 | module TTImp.ProcessBuiltin
  3 |
  4 | import Libraries.Data.NatSet
  5 |
  6 | import Core.Context.Log
  7 | import Core.CompileExpr
  8 | import Core.Env
  9 |
 10 | import TTImp.TTImp
 11 |
 12 | %default covering
 13 |
 14 | showDefType : Def -> String
 15 | showDefType None = "undefined"
 16 | showDefType (PMDef {}) = "function"
 17 | showDefType (ExternDef {}) = "external function"
 18 | showDefType (ForeignDef {}) = "foreign function"
 19 | showDefType (Builtin {}) = "builtin function"
 20 | showDefType (DCon {}) = "data constructor"
 21 | showDefType (TCon {}) = "type constructor"
 22 | showDefType (Hole {}) = "hole"
 23 | showDefType (BySearch {}) = "search"
 24 | showDefType (Guess {}) = "guess"
 25 | showDefType ImpBind = "bound name"
 26 | showDefType (UniverseLevel {}) = "universe level"
 27 | showDefType Delayed = "delayed"
 28 |
 29 | ||| Get the return type.
 30 | getReturnType : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
 31 | getReturnType tm@(Bind _ x b scope) = case b of
 32 |     Let _ _ val _ => getReturnType $ subst {x} val scope
 33 |     Pi {} => getReturnType scope
 34 |     _ => Nothing
 35 | getReturnType tm = Just (vars ** tm)
 36 |
 37 | ||| Get the top level type constructor if there is one.
 38 | getTypeCons : {vars : _} -> Term vars -> Maybe Name
 39 | getTypeCons (Local _ _ _ p) = Just $ nameAt p
 40 | getTypeCons (Ref _ _ name) = Just name
 41 | getTypeCons (Meta {}) = Nothing
 42 | getTypeCons (Bind _ x b scope) = case b of
 43 |     Let _ _ val _ => getTypeCons $ subst {x} val scope
 44 |     _ => Nothing
 45 | getTypeCons (App _ fn _) = getTypeCons fn
 46 | getTypeCons _ = Nothing
 47 |
 48 | ||| Get the arguments of a `Term` representing a type.
 49 | getTypeArgs : {vars : _} -> Term vars -> List (vars ** Term vars)
 50 | getTypeArgs (Bind _ x b tm) = case b of
 51 |     Let _ _ val _ => getTypeArgs $ subst {x} val tm
 52 |     Pi _ _ _ arg => (_ ** arg) :: getTypeArgs tm
 53 |     _ => []
 54 | getTypeArgs _ = []
 55 |
 56 | ||| Get all non-erased aruments.
 57 | getNEArgs : {vars : _} -> Term vars -> List (vars ** Term vars)
 58 | getNEArgs (Bind _ x b tm) = case b of
 59 |     Let _ _ val _ => getNEArgs $ subst {x} val tm
 60 |     Pi _ mul _ arg => if isErased mul
 61 |         then getNEArgs tm
 62 |         else (_ ** arg) :: getNEArgs tm
 63 |     _ => []
 64 | getNEArgs _ = []
 65 |
 66 | ||| Get the first non-erased argument type.
 67 | getFirstNEType : {vars : _} -> Term vars -> Maybe (vars ** Term vars)
 68 | getFirstNEType tm = case getNEArgs tm of
 69 |     [] => Nothing
 70 |     arg :: _ => Just arg
 71 |
 72 | ||| Get the index of the first non-erased argument if it exists.
 73 | getNEIndex : Term vars -> Maybe Nat
 74 | getNEIndex (Bind _ x b tm) = case b of
 75 |     Let _ _ val _ => getNEIndex $ subst {x} val tm
 76 |     Pi _ mul _ arg => if isErased mul
 77 |         then getNEIndex tm
 78 |         else Just 0
 79 |     _ => Nothing
 80 | getNEIndex _ = Nothing
 81 |
 82 | ||| Get the index of all non-erased Integer argument.
 83 | getNEIntegerIndex : Term vars -> Maybe (List Nat)
 84 | getNEIntegerIndex (Bind _ x b tm) = case b of
 85 |     Let _ _ val _ => getNEIntegerIndex $ subst {x} val tm
 86 |     Pi _ mul _ arg => if not (isErased mul) && isInteger arg
 87 |         then Prelude.(::) 0 . map (+ 1) <$> getNEIntegerIndex tm
 88 |         else getNEIntegerIndex tm
 89 |     _ => Nothing
 90 |   where
 91 |     isInteger : forall vars. Term vars -> Bool
 92 |     isInteger (PrimVal _ $ PrT IntegerType) = True
 93 |     isInteger _ = False
 94 | getNEIntegerIndex _ = Just []
 95 |
 96 | ||| Do the terms match ignoring arguments to type constructors.
 97 | termConMatch : Term vs -> Term vs' -> Bool
 98 | termConMatch (Local _ _ x _) (Local _ _ y _) = x == y
 99 | termConMatch (Ref _ _ n) (Ref _ _ m) = n == m
100 | termConMatch (Meta _ _ i args0) (Meta _ _ j args1)
101 |     = i == j && all (uncurry termConMatch) (zip args0 args1)
102 |     -- I don't understand how they're equal if args are different lengths
103 |     -- but this is what's in Core.TT.
104 | termConMatch (Bind _ _ b s) (Bind _ _ c t) = eqBinderBy termConMatch b c && termConMatch s t
105 | termConMatch (App _ f _) (App _ g _) = termConMatch f g
106 | termConMatch (As _ _ a p) (As _ _ b q) = termConMatch a b && termConMatch p q
107 | termConMatch (TDelayed _ _ tm0) tm1 = termConMatch tm0 tm1
108 | termConMatch tm0 (TDelayed _ _ tm1) = termConMatch tm0 tm1
109 |     -- don't check for laziness here to give more accurate error messages.
110 | termConMatch (TDelay _ _ tm0 x0) (TDelay _ _ tm1 x1) = termConMatch tm0 tm1 && termConMatch x0 x1
111 | termConMatch (TForce _ _ tm0) tm1 = termConMatch tm0 tm1
112 | termConMatch tm0 (TForce _ _ tm1) = termConMatch tm0 tm1
113 | termConMatch (PrimVal {}) (PrimVal {}) = True -- no constructor to check.
114 | termConMatch (Erased {}) (Erased {}) = True -- return type can't erased?
115 | termConMatch (TType {}) (TType {}) = True
116 | termConMatch _ _ = False
117 |
118 | ||| Check a type is strict.
119 | isStrict : Term vs -> Bool
120 | isStrict (Local {}) = True
121 | isStrict (Ref {}) = True
122 | isStrict (Meta _ _ i args) = all isStrict args
123 | isStrict (Bind _ _ b s) = isStrict (binderType b) && isStrict s
124 | isStrict (App _ f x) = isStrict f && isStrict x
125 | isStrict (As _ _ a p) = isStrict a && isStrict p
126 | isStrict (TDelayed {}) = False
127 | isStrict (TDelay _ _ f x) = isStrict f && isStrict x
128 | isStrict (TForce _ _ tm) = isStrict tm
129 | isStrict (PrimVal {}) = True
130 | isStrict (Erased {}) = True
131 | isStrict (TType {}) = True
132 |
133 | ||| Get the name and definition of a list of names.
134 | getConsGDef :
135 |     Ref Ctxt Defs =>
136 |     FC -> (cons : List Name) ->
137 |     Core $ List (Name, GlobalDef)
138 | getConsGDef fc cons = do
139 |     defs <- get Ctxt
140 |     let c = defs.gamma
141 |     for cons $ \n => do
142 |         [(n', _, gdef)] <- lookupCtxtName n c
143 |             | ns => ambiguousName fc n $ (\(n, _, _) => n) <$> ns
144 |         pure (n', gdef)
145 |
146 | isNatural : Ref Ctxt Defs => FC ->Name -> Core Bool
147 | isNatural fc n = do
148 |     defs <- get Ctxt
149 |     Just gdef <- lookupCtxtExact n defs.gamma
150 |         | Nothing => undefinedName EmptyFC n
151 |     let TCon _ _ _ _ _ cons _ = gdef.definition
152 |         | _ => pure False
153 |     consDefs <- getConsGDef fc (fromMaybe [] cons)
154 |     pure $ all hasNatFlag consDefs
155 |   where
156 |     isNatFlag : DefFlag -> Bool
157 |     isNatFlag (ConType ZERO) = True
158 |     isNatFlag (ConType SUCC) = True
159 |     isNatFlag _ = False
160 |     hasNatFlag : (Name, GlobalDef) -> Bool
161 |     hasNatFlag (_, gdef) = any isNatFlag gdef.flags
162 |
163 | ||| Check a list of constructors has exactly
164 | ||| 1 'Z'-like constructor
165 | ||| and 1 `S`-like constructor, which has type `ty -> ty` or `ty arg -> `ty (f arg)`.
166 | checkNatCons : Context -> (cons : List (Name, GlobalDef)) -> (dataType : Name) -> FC -> Core ()
167 | checkNatCons c cons ty fc = case !(foldr checkCon (pure (Nothing, Nothing)) cons) of
168 |     (Just zero, Just succ) => pure ()
169 |     (Nothing, _) => throw $ GenericMsg fc $ "No 'Z'-like constructors for " ++ show ty ++ "."
170 |     (_, Nothing) => throw $ GenericMsg fc $ "No 'S'-like constructors for " ++ show ty ++ "."
171 |   where
172 |     ||| Check if a list of names contains a name.
173 |     checkSArgType : List Name -> Core ()
174 |     checkSArgType [] = throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " is missing argument of type: " ++ show ty
175 |     checkSArgType (n :: ns) = if nameRoot n == nameRoot ty && (n `matches` ty)
176 |         then checkSArgType ns
177 |         else throw $ GenericMsg fc $ "'S'-like constructor for " ++ show ty ++ " has unexpected argument: " ++ show n
178 |
179 |     ||| Check the type of an 'S'-like constructor.
180 |     checkTyS : Name -> GlobalDef -> Core ()
181 |     checkTyS n gdef = do
182 |         let type = gdef.type
183 |             erase = gdef.eraseArgs
184 |         let Just (_ ** arg) = getFirstNEType type
185 |             | Nothing => throw $ InternalError "Expected a non-erased argument, found none."
186 |         let Just (_ ** ret) = getReturnType type
187 |             | Nothing => throw $ InternalError $ "Unexpected type " ++ show type
188 |         unless (termConMatch arg ret) $ throw $ GenericMsg fc $ "Incorrect type for 'S'-like constructor for " ++ show ty ++ "."
189 |         unless (isStrict arg) $ throw $ GenericMsg fc $ "Natural builtin does not support lazy types."
190 |         pure ()
191 |
192 |     ||| Check a constructor's arity and type.
193 |     -- 'Z'-like constructor is always first, then 'S'-like constructor.
194 |     checkCon : (Name, GlobalDef) -> Core (Maybe Name, Maybe Name) -> Core (Maybe Name, Maybe Name)
195 |     checkCon (n, gdef) cons = do
196 |         (zero, succ) <- cons
197 |         let DCon _ arity _ = gdef.definition
198 |             | def => throw $ GenericMsg fc $ "Expected data constructor, found:" ++ showDefType def
199 |         case arity `minus` size gdef.eraseArgs of
200 |             0 => case zero of
201 |                 Just _ => throw $ GenericMsg fc $ "Multiple 'Z'-like constructors for " ++ show ty ++ "."
202 |                 Nothing => pure (Just n, succ)
203 |             1 => case succ of
204 |                 Just _ => throw $ GenericMsg fc $ "Multiple 'S'-like constructors for " ++ show ty ++ "."
205 |                 Nothing => do
206 |                     checkTyS n gdef
207 |                     pure (zero, Just n)
208 |             _ => throw $ GenericMsg fc $ "Constructor " ++ show n ++ " doesn't match any pattern for Natural."
209 |
210 | ||| Check a `%builtin Natural` pragma is correct.
211 | processBuiltinNatural :
212 |     Ref Ctxt Defs =>
213 |     FC -> Name -> Core ()
214 | processBuiltinNatural fc name = do
215 |     ds <- get Ctxt
216 |     log "builtin.Natural" 5 $ "Processing %builtin Natural " ++ show name ++ "."
217 |     [(n, _, gdef)] <- lookupCtxtName name ds.gamma
218 |         | ns => ambiguousName fc name $ (\(n, _, _) => n) <$> ns
219 |     False <- isNatural fc n
220 |         | True => pure ()
221 |     let TCon _ _ _ _ _ dcons _ = gdef.definition
222 |         | def => throw $ GenericMsg fc
223 |             $ "Expected a type constructor, found " ++ showDefType def ++ "."
224 |     cons <- getConsGDef fc (fromMaybe [] dcons)
225 |     checkNatCons ds.gamma cons n fc
226 |
227 | ||| Check a `%builtin NaturalToInteger` pragma is correct.
228 | processNatToInteger :
229 |     Ref Ctxt Defs =>
230 |     FC -> Name -> Core ()
231 | processNatToInteger fc fn = do
232 |     let show_fn = show fn
233 |     ds <- get Ctxt
234 |     log "builtin.NaturalToInteger" 5 $ "Processing %builtin NaturalToInteger " ++ show_fn ++ "."
235 |     [(_ , i, gdef)] <- lookupCtxtName fn ds.gamma
236 |         | ns => ambiguousName fc fn $ (\(n, _, _) => n) <$> ns
237 |     let PMDef _ args _ cases _ = gdef.definition
238 |         | def => throw $ GenericMsg fc
239 |             $ "Expected function definition, found " ++ showDefType def ++ "."
240 |     type <- toFullNames gdef.type
241 |     logTerm "builtin.NaturalToInteger" 25 ("Type of " ++ show_fn) type
242 |     let [(_ ** arg)] = getNEArgs type
243 |         | [] => throw $ GenericMsg fc $ "No arguments found for " ++ show_fn ++ "."
244 |         | _ => throw $ GenericMsg fc $ "More than 1 non-erased arguments found for " ++ show_fn ++ "."
245 |     let Just tyCon = getTypeCons arg
246 |         | Nothing => throw $ GenericMsg fc
247 |             $ "No type constructor found for non-erased arguement of " ++ show_fn ++ "."
248 |     True <- isNatural fc tyCon
249 |         | False => throw $ GenericMsg fc $ "Non-erased argument is not a 'Nat'-like type."
250 |     let Just natIdx = getNEIndex type
251 |         | Nothing => throw $ InternalError "Couldn't find non-erased argument."
252 |     setFlag fc (Resolved i) $ Identity natIdx
253 |
254 | ||| Check a `%builtin IntegerToNatural` pragma is correct.
255 | processIntegerToNat :
256 |     Ref Ctxt Defs =>
257 |     FC -> Name -> Core ()
258 | processIntegerToNat fc fn = do
259 |     let show_fn = show fn
260 |     ds <- get Ctxt
261 |     log "builtin.IntegerToNatural" 5 $ "Processing %builtin IntegerToNatural " ++ show_fn ++ "."
262 |     [(_, i, gdef)] <- lookupCtxtName fn ds.gamma
263 |         | ns => ambiguousName fc fn $ (\(n, _, _) => n) <$> ns
264 |     type <- toFullNames gdef.type
265 |     let PMDef _ _ _ _ _ = gdef.definition
266 |         | def => throw $ GenericMsg fc
267 |             $ "Expected function definition, found " ++ showDefType def ++ "."
268 |     logTerm "builtin.IntegerToNatural" 25 ("Type of " ++ show_fn) type
269 |     let Just [intIdx] = getNEIntegerIndex type
270 |         | Just [] => throw $ GenericMsg fc $ "No unrestricted arguments of type `Integer` found for " ++ show_fn ++ "."
271 |         | Just _ => throw $ GenericMsg fc $ "More than one unrestricted arguments of type `Integer` found for " ++ show_fn ++ "."
272 |         | Nothing => throw $ InternalError
273 |             $ "Unexpected arity while processing %builtin IntegerToNatural " ++ show_fn ++ " (getNEIntegerIndex returned Nothing)"
274 |     let Just (_ ** retTy) = getReturnType type
275 |         | Nothing => throw $ InternalError $ "Unexpected type " ++ show type
276 |     let Just retCon = getTypeCons retTy
277 |         | Nothing => throw $ GenericMsg fc
278 |             $ "No type constructor found for return type of " ++ show_fn ++ "."
279 |     True <- isNatural fc retCon
280 |         | False => throw $ GenericMsg fc $ "Return type is not a 'Nat'-like type"
281 |     setFlag fc (Resolved i) $ Identity intIdx
282 |
283 | ||| Check a `%builtin` pragma is correct.
284 | export
285 | processBuiltin :
286 |     Ref Ctxt Defs =>
287 |     NestedNames vars -> Env Term vars -> FC -> BuiltinType -> Name -> Core ()
288 | processBuiltin nest env fc type name = do
289 |     case type of
290 |         BuiltinNatural => processBuiltinNatural fc name
291 |         NaturalToInteger => processNatToInteger fc name
292 |         IntegerToNatural => processIntegerToNat fc name
293 |