0 | module Idrall.Check

  2 | import Idrall.Expr

  3 | import Idrall.Error

  4 | import Idrall.Value

  5 | import Idrall.Map

  6 | import Idrall.Eval

  8 | import Data.List

  9 | import Data.List1

 10 | import Data.String

 12 | countName' : Name -> List Name -> Int

 13 | countName' x env = go 0 env

 15 |   go : Int -> List Name -> Int

 16 |   go acc [] = acc

 17 |   go acc (x' :: xs) = go (if x == x' then acc + 1 else acc) xs

 19 | fresh : Name -> List Name -> (Name, Value)

 20 | fresh x env = (x, VVar initFC x (countName' x env))

 22 | freshCl : Closure -> List Name -> (Name, Value, Closure)

 23 | freshCl cl@(MkClosure x _ _) env = (x, snd (fresh x env), cl)

 26 |   qVar : FC -> Name -> Int -> List Name -> Expr Void

 27 |   qVar fc x i env = EVar fc x ((countName' x env) - i - 1)

 29 |   quoteBind : Name -> List Name -> Value -> Either Error (Expr Void)

 30 |   quoteBind x env = quote (x :: env)

 32 |   qApp : FC -> List Name -> Expr Void -> Value -> Either Error (Expr Void)

 33 |   qApp _ env t (VPrimVar fc) = pure $ t

 34 |   qApp fc env t u        = pure $ EApp fc t !(quote env u)

 36 |   -- Prelude.foldlM : (Foldable t, Monad m) => (a -> b -> m a) -> a -> t b -> m a

 37 |   qAppM : FC -> List Name -> Expr Void -> List Value -> Either Error (Expr Void)

 38 |   qAppM fc env x args = foldlM (qApp fc env) x args

 40 |   export

 41 |   quote : List Name -> Value -> Either Error (Expr Void)

 42 |   quote env (VConst fc k) = pure $ EConst fc k

 43 |   quote env (VVar fc x i) = pure $ qVar fc x i env

 44 |   quote env (VApp fc t u) = qApp fc env !(quote env t) u

 45 |   quote env (VLambda fc a b) =

 46 |     let (x, v, t) = freshCl b env in

 47 |         pure $ ELam fc x !(quote env a) !(quoteBind x env !(inst t v))

 48 |   quote env (VHLam fc (Typed x a) t) =

 49 |     let (x', v) = fresh x env in

 50 |     pure $ ELam fc x' !(quote env a) !(quoteBind x env !(t v))

 51 |   quote env (VHLam fc NaturalSubtractZero _) =

 52 |     pure $ EApp fc (ENaturalSubtract (fcToVFC fc)) (ENaturalLit (fcToVFC fc) 0)

 53 |   quote env (VHLam fc _ t) = quote env !(t $ VPrimVar (fcToVFC fc))

 54 |   quote env (VPi fc a b) =

 55 |     let (x, v, b') = freshCl b env in

 56 |         pure $ EPi fc x !(quote env a) !(quoteBind x env !(inst b' v))

 57 |   quote env (VHPi fc x a b) =

 58 |     let (x', v) = fresh x env in

 59 |         pure $ EPi fc x !(quote env a) !(quoteBind x env !(b v))

 60 |   quote env (VBool fc) = pure $ EBool fc

 61 |   quote env (VBoolLit fc b) = pure $ EBoolLit fc b

 62 |   quote env (VBoolAnd fc t u) = pure $ EBoolAnd fc !(quote env t) !(quote env u)

 63 |   quote env (VBoolOr fc t u) = pure $ EBoolOr fc !(quote env t) !(quote env u)

 64 |   quote env (VBoolEQ fc t u) = pure $ EBoolEQ fc !(quote env t) !(quote env u)

 65 |   quote env (VBoolNE fc t u) = pure $ EBoolNE fc !(quote env t) !(quote env u)

 66 |   quote env (VBoolIf fc b t f) = pure $ EBoolIf fc !(quote env b) !(quote env t) !(quote env f)

 67 |   quote env (VNatural fc) = pure $ ENatural fc

 68 |   quote env (VNaturalLit fc k) = pure $ ENaturalLit fc k

 69 |   quote env (VNaturalBuild fc x) = qApp fc env (ENaturalBuild fc) x

 70 |   quote env (VNaturalFold fc w x y z) = qAppM fc env (ENaturalFold fc) [w, x, y, z]

 71 |   quote env (VNaturalIsZero fc x) = qApp fc env (ENaturalIsZero fc) x

 72 |   quote env (VNaturalEven fc x) = qApp fc env (ENaturalEven fc) x

 73 |   quote env (VNaturalOdd fc x) = qApp fc env (ENaturalOdd fc) x

 74 |   quote env (VNaturalToInteger fc x) = qApp fc env (ENaturalToInteger fc) x

 75 |   quote env (VNaturalSubtract fc x y) = qAppM fc env (ENaturalSubtract fc) [x, y]

 76 |   quote env (VNaturalShow fc x) = qApp fc env (ENaturalShow fc) x

 77 |   quote env (VNaturalPlus fc t u) = pure $ ENaturalPlus fc !(quote env t) !(quote env u)

 78 |   quote env (VNaturalTimes fc t u) = pure $ ENaturalTimes fc !(quote env t) !(quote env u)

 79 |   quote env (VInteger fc) = pure $ EInteger fc

 80 |   quote env (VIntegerLit fc x) = pure $ EIntegerLit fc x

 81 |   quote env (VIntegerShow fc x) = qApp fc env (EIntegerShow fc) x

 82 |   quote env (VIntegerNegate fc x) = qApp fc env (EIntegerNegate fc) x

 83 |   quote env (VIntegerClamp fc x) = qApp fc env (EIntegerClamp fc) x

 84 |   quote env (VIntegerToDouble fc x) = qApp fc env (EIntegerToDouble fc) x

 85 |   quote env (VDouble fc) = pure $ EDouble fc

 86 |   quote env (VDoubleLit fc x) = pure $ EDoubleLit fc x

 87 |   quote env (VDoubleShow fc x) = qApp fc env (EDoubleShow fc) x

 88 |   quote env (VText fc) = pure $ EText fc

 89 |   quote env (VTextLit fc (MkVChunks xs x)) =

 90 |     let chx = traverse (mapChunks (quote env)) xs in

 91 |     pure $ ETextLit fc (MkChunks !chx x)

 92 |   quote env (VTextAppend fc t u) = pure $ ETextAppend fc !(quote env t) !(quote env u)

 93 |   quote env (VTextShow fc t) = qApp fc env (ETextShow fc) t

 94 |   quote env (VTextReplace fc t u v) = qAppM fc env (ETextReplace fc) [t, u, v]

 95 |   quote env (VList fc x) = qApp fc env (EList fc) x

 96 |   quote env (VListLit fc Nothing ys) =

 97 |     let ys' = traverse (quote env) ys in

 98 |     pure $ EListLit fc Nothing !ys'

 99 |   quote env (VListLit fc (Just x) ys) =

100 |     let ys' = traverse (quote env) ys in

101 |     pure $ EListLit fc (Just !(quote env x)) !ys'

102 |   quote env (VListAppend fc x y) = pure $ EListAppend fc !(quote env x) !(quote env y)

103 |   quote env (VListBuild fc t u) = qAppM fc env (EListBuild fc) [t, u]

104 |   quote env (VListFold fc a l t u v) = qAppM fc env (EListFold fc) [a, l, t, u, v]

105 |   quote env (VListLength fc t u) = qAppM fc env (EListLength fc) [t, u]

106 |   quote env (VListHead fc t u) = qAppM fc env (EListHead fc) [t, u]

107 |   quote env (VListLast fc t u) = qAppM fc env (EListLast fc) [t, u]

108 |   quote env (VListIndexed fc t u) = qAppM fc env (EListIndexed fc) [t, u]

109 |   quote env (VListReverse fc t u) = qAppM fc env (EListReverse fc) [t, u]

110 |   quote env (VOptional fc x) = qApp fc env (EOptional fc) x

111 |   quote env (VNone fc x) = qApp fc env (ENone fc) x

112 |   quote env (VSome fc x) = pure $ ESome fc !(quote env x)

113 |   quote env (VEquivalent fc x y) = pure $ EEquivalent fc !(quote env x) !(quote env y)

114 |   quote env (VAssert fc x) = pure $ EAssert fc !(quote env x)

115 |   quote env (VRecord fc x) =

116 |     let x' = traverse (quote env) x in

117 |     pure $ ERecord fc !x'

118 |   quote env (VRecordLit fc x) =

119 |     let x' = traverse (quote env) x in

120 |     pure $ ERecordLit fc !x'

121 |   quote env (VUnion fc x) =

122 |     let x' = traverse (mapMaybe (quote env)) x in

123 |     pure $ EUnion fc !x'

124 |   quote env (VCombine fc x y) = pure $ ECombine fc !(quote env x) !(quote env y)

125 |   quote env (VCombineTypes fc x y) = pure $ ECombineTypes fc !(quote env x) !(quote env y)

126 |   quote env (VPrefer fc x y) = pure $ EPrefer fc !(quote env x) !(quote env y)

127 |   quote env (VMerge fc x y Nothing) = pure $ EMerge fc !(quote env x) !(quote env y) Nothing

128 |   quote env (VMerge fc x y (Just z)) = pure $ EMerge fc !(quote env x) !(quote env y) (Just !(quote env z))

129 |   quote env (VToMap fc x Nothing) = pure $ EToMap fc !(quote env x) Nothing

130 |   quote env (VToMap fc x (Just y)) = pure $ EToMap fc !(quote env x) (Just !(quote env y))

131 |   quote env (VField fc x y) = pure $ EField fc !(quote env x) y

132 |   quote env (VInject fc m k Nothing) =

133 |     let m' = traverse (mapMaybe (quote env)) m in

134 |     pure $ EField fc (EUnion (fcToVFC fc) !m') k

135 |   quote env (VInject fc m k (Just t)) =

136 |     let m' = traverse (mapMaybe (quote env)) m in

137 |     qApp fc env (EField fc (EUnion (fcToVFC fc) !m') k) t

138 |   quote env (VProject fc t (Left ks)) = pure $ EProject fc !(quote env t) (Left ks)

139 |   quote env (VProject fc t (Right u)) = pure $ EProject fc !(quote env t) (pure $ !(quote env u))

140 |   quote env (VWith fc t ks u) = pure $ EWith fc !(quote env t) ks !(quote env u)

141 |   quote env (VPrimVar fc) = Left $ ReadBackError fc "Can't quote VPrimVar"

144 | vAnyPi : Value -> Either Error (Name, Ty, (Value -> Either Error Value))

145 | vAnyPi (VHPi fc x a b) = pure (x, a, b)

146 | vAnyPi (VPi fc a b@(MkClosure x _ _)) = pure (x, a, inst b)

147 | vAnyPi t = Left $ Unexpected (getFC t) $ show t ++ " is not a VPi or VHPi"

149 | data Types = TEmpty

150 |            | TBind Types Name Value

153 | Show Types where

154 |   show TEmpty = "TEmpty"

155 |   show (TBind x y z) = "(TBind " ++ show x ++ " " ++ show y ++ " " ++ show z ++ ")"

157 | axiom : FC -> U -> Either Error U

158 | axiom fc CType = pure Kind

159 | axiom fc Kind = pure Sort

160 | axiom fc Sort = Left $ SortError fc

162 | rule : U -> U -> U

163 | rule CType CType = CType

164 | rule Kind CType = CType

165 | rule Sort CType = CType

166 | rule CType Kind = Kind

167 | rule Kind Kind = Kind

168 | rule Sort Kind = Sort

169 | rule CType Sort = Sort

170 | rule Kind Sort = Sort

171 | rule Sort Sort = Sort

173 | record Cxt where

174 |   constructor MkCxt

175 |   values : Env

176 |   types  : Types

179 | Show Cxt where

180 |   show x = "(MkCxt { values = " ++ show (values x) ++ ", types = " ++ show 2 ++ "})"

183 | initCxt : Cxt

184 | initCxt = MkCxt Empty TEmpty

186 | envNames : Env -> List Name

187 | envNames Empty = []

188 | envNames (Skip env x) = x :: envNames env

189 | envNames (Extend env x _) = x :: envNames env

192 | define : Name -> Value -> Ty -> Cxt -> Cxt

193 | define x t a (MkCxt ts as) = MkCxt (Extend ts x t) (TBind as x a)

196 | bind : Name -> Value -> Cxt -> Cxt

197 | bind x a (MkCxt ts as) = MkCxt (Skip ts x) (TBind as x a)

200 |   unify : Cxt -> Value -> Value -> Either Error ()

201 |   unify cxt t u = conv (values cxt) t u

203 |   ||| Check if an Expr is of type `VConst c`

204 |   checkTy : Cxt -> Expr Void -> Either Error (Expr Void, U)

205 |   checkTy cxt t = do

206 |     (t, a) <- infer cxt t

207 |     case a of

208 |       VConst fc c => pure (t, c)

209 |       other        => Left $ ErrorMessage (getFC other) $ show other ++ " is not a Type/Kind/Sort"

211 |   ||| returns the original `Expr Void` on success

212 |   export

213 |   check : Cxt -> Expr Void -> Value -> Either Error (Expr Void)

214 |   check cxt (EConst fc CType) vKype = pure $ EConst fc CType

215 |   check cxt (EConst fc Kind) vSort = pure $ EConst fc Kind

216 |   check cxt (EConst fc Sort) z = Left $ SortError fc

217 |   check cxt (ELam fc x a t) pi =

218 |     let (x', v) = fresh x (envNames (values cxt)) in do -- TODO not sure about fresh...

219 |     (_, a', b) <- vAnyPi pi

220 |     (a, _) <- checkTy cxt a

221 |     av <- eval (values cxt) a

222 |     unify cxt av a'

223 |     t <- check (define x' v av cxt) t !(b v)

224 |     pure $ ELam fc x a t

225 |   check cxt (EBoolLit fc t) (VBool fc') = pure $ EBoolLit fc t

226 |   check cxt (ENaturalLit fc t) (VNatural fc') = pure $ ENaturalLit fc t

227 |   check cxt (EIntegerLit fc t) (VInteger fc') = pure $ EIntegerLit fc t

228 |   check cxt (EDoubleLit fc t) (VDouble fc') = pure $ EDoubleLit fc t

229 |   check cxt (ETextLit fc t) (VText fc') = pure $ ETextLit fc t

230 |   -- check cxt (ERecordLit y) z = ?check_rhs TODO maybe add this later for performance?

231 |   check cxt t a = do

232 |     (t, a') <- infer cxt t

233 |     unify cxt a' a

234 |     pure t

236 |   unexpected : String -> Value -> Either Error a

237 |   unexpected str v = Left (Unexpected (getFC v) $ str ++ " Value: " ++ show v)

239 |   natFoldTy : FC -> Value

240 |   natFoldTy fc =

241 |     VHPi fc "natural" vType $ \natural =>

242 |     pure $ VHPi fc "succ" (vFun natural natural) $ \succ =>

243 |     pure $ VHPi fc "zero" natural $ \zero =>

244 |     pure $ natural

246 |   listFoldTy : FC -> Value -> Value

247 |   listFoldTy fc a =

248 |     VHPi fc "list" vType $ \list =>

249 |     pure $ VHPi fc "cons" (vFun a $ vFun list list) $ \cons =>

250 |     pure $ VHPi fc "nil" list $ \nil =>

251 |     pure $ list

253 |   ||| returns a pair (Expr, Value), which is original Expr, and it's type as a Value

254 |   export

255 |   infer : Cxt -> Expr Void -> Either Error (Expr Void, Value)

256 |   infer cxt (EConst fc k) = (\k' => (EConst fc k, VConst fc k')) <$> axiom fc k

257 |   infer cxt (EVar fc x i) = go (types cxt) i

258 |   where

259 |     go : Types -> Int -> Either Error (Expr Void, Value)

260 |     go TEmpty n = Left $ MissingVar fc $ x ++ "@" ++ show i ++ "\n in Cxt: " ++ show cxt

261 |     go (TBind ts x' a) n =

262 |       case x == x' of

263 |            True => if n == 0 then pure (EVar fc x i, a) else go ts (n - 1)

264 |            False => go ts n

265 |   infer cxt (ELam fc x a t) = do

266 |     (a, ak) <- checkTy cxt a

267 |     av <- eval (values cxt) a

268 |     (t, b) <- infer (bind x av cxt) t

269 |     nb <- quote (x :: (envNames (values cxt))) b

270 |     pure ( ELam fc x a t

271 |           , VHPi fc x av $

272 |             \u => pure $ !(eval (Extend (values cxt) x u) nb)) -- TODO check i'm using values right

273 |   infer cxt (EPi fc x a b) = do

274 |     (a, ak) <- checkTy cxt a

275 |     av <- eval (values cxt) a

276 |     (b, bk) <- checkTy (bind x av cxt) b

277 |     pure (EPi fc x a b, VConst fc $ rule ak bk)

278 |   infer cxt (EApp fc t u) = do

279 |     (t, tt) <- infer cxt t

280 |     (x, a, b) <- vAnyPi tt

281 |     _ <- check cxt u a

282 |     pure $ (EApp fc t u, !(b !(eval (values cxt) u)))

283 |   infer cxt (ELet fc x Nothing a b) = do

284 |     (a, aa) <- infer cxt a

285 |     v <- eval (values cxt) a

286 |     infer (define x v aa cxt) b

287 |   infer cxt (ELet fc x (Just t) a b) = do

288 |     tt <- eval (values cxt) t

289 |     _ <- check cxt a tt

290 |     v <- eval (values cxt) a

291 |     infer (define x v tt cxt) b

292 |   infer cxt (EAnnot fc x t) = do

293 |     tv <- eval (values cxt) t

294 |     _ <- check cxt x tv

295 |     pure $ (EAnnot fc x t, tv)

296 |   infer cxt (EBool fc) = pure $ (EBool fc, VConst fc CType)

297 |   infer cxt (EBoolLit fc x) = pure $ (EBoolLit fc x, VBool fc)

298 |   infer cxt (EBoolAnd fc x y) = do

299 |     _ <- check cxt x (VBool fc)

300 |     _ <- check cxt y (VBool fc)

301 |     pure $ (EBoolAnd fc x y, VBool fc)

302 |   infer cxt (EBoolOr fc x y) = do

303 |     _ <- check cxt x (VBool initFC)

304 |     _ <- check cxt y (VBool initFC)

305 |     pure $ (EBoolOr fc x y, VBool fc)

306 |   infer cxt (EBoolEQ fc x y) = do

307 |     _ <- check cxt x (VBool initFC)

308 |     _ <- check cxt y (VBool initFC)

309 |     pure $ (EBoolEQ fc x y, VBool fc)

310 |   infer cxt (EBoolNE fc x y) = do

311 |     _ <- check cxt x (VBool initFC)

312 |     _ <- check cxt y (VBool initFC)

313 |     pure $ (EBoolNE fc x y, VBool fc)

314 |   infer cxt (EBoolIf fc b t f) = do

315 |     _ <- check cxt b (VBool initFC)

316 |     (t, tt) <- infer cxt t

317 |     _ <- check cxt f tt

318 |     pure $ (EBoolIf fc b t f, tt)

319 |   infer cxt (ENatural fc) = pure $ (ENatural fc, VConst (fcToVFC fc) CType)

320 |   infer cxt (ENaturalLit fc k) = pure $ (ENaturalLit fc k, VNatural (fcToVFC fc))

321 |   infer cxt (ENaturalBuild fc) = pure $ (ENaturalBuild fc, vFun (natFoldTy (fcToVFC fc)) (VNatural (fcToVFC fc)))

322 |   infer cxt (ENaturalFold fc) = pure (ENaturalFold fc, vFun (VNatural (fcToVFC fc)) (natFoldTy (fcToVFC fc)))

323 |   infer cxt (ENaturalIsZero fc) = pure $ (ENaturalIsZero fc, (vFun (VNatural (fcToVFC fc)) (VBool (fcToVFC fc))))

324 |   infer cxt (ENaturalEven fc) = pure $ (ENaturalEven fc, (vFun (VNatural (fcToVFC fc)) (VBool (fcToVFC fc))))

325 |   infer cxt (ENaturalOdd fc) = pure $ (ENaturalOdd fc, (vFun (VNatural (fcToVFC fc)) (VBool (fcToVFC fc))))

326 |   infer cxt (ENaturalSubtract fc) = pure $ (ENaturalOdd fc, (vFun (VNatural (fcToVFC fc)) (vFun (VNatural (fcToVFC fc)) (VNatural (fcToVFC fc)))))

327 |   infer cxt (ENaturalToInteger fc) = pure $ (ENaturalToInteger fc, (vFun (VNatural (fcToVFC fc)) (VInteger (fcToVFC fc))))

328 |   infer cxt (ENaturalShow fc) = pure $ (ENaturalShow (fcToVFC fc), (vFun (VNatural (fcToVFC fc)) (VText (fcToVFC fc))))

329 |   infer cxt (ENaturalPlus fc t u) = do

330 |     _ <- check cxt t (VNatural initFC)

331 |     _ <- check cxt u (VNatural initFC)

332 |     pure $ (ENaturalPlus fc t u, VNatural fc)

333 |   infer cxt (ENaturalTimes fc t u) = do

334 |     _ <- check cxt t (VNatural initFC)

335 |     _ <- check cxt u (VNatural initFC)

336 |     pure $ (ENaturalTimes fc t u, VNatural $ fcToVFC fc)

337 |   infer cxt (EInteger fc) = pure $ (EInteger fc, VConst (fcToVFC fc) CType)

338 |   infer cxt (EIntegerLit fc x) = pure $ (EIntegerLit fc x, VInteger (fcToVFC fc))

339 |   infer cxt (EIntegerShow fc) = pure $ (EIntegerShow fc, (vFun (VInteger (fcToVFC fc)) (VText (fcToVFC fc))))

340 |   infer cxt (EIntegerNegate fc) = pure $ (EIntegerNegate fc, (vFun (VInteger (fcToVFC fc)) (VInteger (fcToVFC fc))))

341 |   infer cxt (EIntegerClamp fc) = pure $ (EIntegerNegate fc, (vFun (VInteger (fcToVFC fc)) (VNatural (fcToVFC fc))))

342 |   infer cxt (EIntegerToDouble fc) = pure $ (EIntegerNegate fc, (vFun (VInteger (fcToVFC fc)) (VDouble (fcToVFC fc))))

343 |   infer cxt (EDouble fc) = pure $ (EDouble fc, VConst fc CType)

344 |   infer cxt (EDoubleLit fc x) = pure $ (EDoubleLit fc x, VDouble fc)

345 |   infer cxt (EDoubleShow fc) = pure $ (EDoubleShow fc, (vFun (VDouble $ fcToVFC fc) (VText $ fcToVFC fc)))

346 |   infer cxt (EText fc) = pure $ (EText fc, VConst (fcToVFC fc) CType)

347 |   infer cxt (ETextLit fc (MkChunks xs x)) =

348 |     let go = mapChunks (\e => check cxt e (VText (fcToVFC fc))) in do

349 |     _ <- traverse go xs

350 |     pure $ (ETextLit fc (MkChunks xs x), (VText (fcToVFC fc)))

351 |   infer cxt (ETextAppend fc t u) = do

352 |     _ <- check cxt t (VText initFC)

353 |     _ <- check cxt u (VText initFC)

354 |     pure $ (ETextAppend fc t u, VText (fcToVFC fc))

355 |   infer cxt (ETextShow fc) = pure $ (EIntegerShow fc, (vFun (VText (fcToVFC fc)) (VText (fcToVFC fc))))

356 |   infer cxt (ETextReplace fc) =

357 |     pure ( ETextReplace fc,

358 |            VHPi fc "needle" (VText (fcToVFC fc)) $ \needle =>

359 |            pure $ VHPi fc "replacement" (VText (fcToVFC fc)) $ \replacement =>

360 |            pure $ VHPi fc "haystack" (VText (fcToVFC fc)) $ \haystack =>

361 |            pure $ VText (fcToVFC fc))

362 |   infer cxt (EList fc) = do

363 |     pure $ (EList fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vType)

364 |   infer cxt (EListLit fc Nothing []) = do

365 |     Left $ ErrorMessage fc "Not type for list" -- TODO better error message

366 |   infer cxt (EListLit fc Nothing (x :: xs)) = do

367 |     (x', ty) <- infer cxt x

368 |     _ <- traverse (\e => check cxt e ty) xs

369 |     pure $ (EListLit fc Nothing (x :: xs), VList (fcToVFC fc) ty)

370 |   infer cxt (EListLit fc (Just a) []) = do

371 |     case !(eval (values cxt) a) of

372 |          VList _ a' => do

373 |            ea' <- quote (envNames $ values cxt) a'

374 |            _ <- check cxt ea' (VConst initFC CType)

375 |            pure $ (EListLit fc (Just a) [], VList (fcToVFC fc) a')

376 |          other => Left $ ErrorMessage fc $ "Not a list annotation: " ++ show other

377 |   infer cxt (EListLit fc (Just a) (x :: xs)) = do

378 |     ty <- eval (values cxt) a

379 |     (a', av) <- infer cxt x

380 |     _ <- traverse (\e => check cxt e av) xs

381 |     _ <- conv (values cxt) ty (VList initFC av)

382 |     pure $ (EListLit fc (Just a) (x :: xs), ty)

383 |   infer cxt (EListAppend fc t u) = do

384 |     (t', tt) <- infer cxt t

385 |     case tt of

386 |          (VList _ x) => do

387 |            _ <- check cxt u tt

388 |            pure $ (EListAppend fc t u, tt)

389 |          _ => Left $ ListAppendError fc "not a list" -- TODO better error message

390 |   infer cxt (EListBuild fc) =

391 |     pure (EListBuild fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vFun (listFoldTy (fcToVFC fc) a) (VList (fcToVFC fc) a))

392 |   infer cxt (EListFold fc) =

393 |     pure (EListFold fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vFun (VList (fcToVFC fc) a) (listFoldTy (fcToVFC fc) a))

394 |   infer cxt (EListLength fc) =

395 |     pure (EListLength fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vFun (VList (fcToVFC fc) a) (VNatural (fcToVFC fc)))

396 |   infer cxt (EListHead fc) =

397 |     pure (EListHead fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vFun (VList (fcToVFC fc) a) (VOptional (fcToVFC fc) a))

398 |   infer cxt (EListLast fc) =

399 |     pure (EListLast fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vFun (VList (fcToVFC fc) a) (VOptional (fcToVFC fc) a))

400 |   infer cxt (EListIndexed fc) =

401 |     pure (EListIndexed fc

402 |          , VHPi fc "a" vType $ \a =>

403 |            pure $ vFun (VList (fcToVFC fc) a)

404 |                   (VList fc (VRecord (fcToVFC fc) (fromList [(MkFieldName "index", VNatural (fcToVFC fc)), (MkFieldName "value", a)]))))

405 |   infer cxt (EListReverse fc) =

406 |     pure (EListReverse fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vFun (VList (fcToVFC fc) a) (VList (fcToVFC fc) a))

407 |   infer cxt (EOptional fc) =

408 |     pure $ (EOptional fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ vType)

409 |   infer cxt (ESome fc t) = do

410 |     (t, tt) <- infer cxt t

411 |     _ <- check cxt !(quote (envNames $ values cxt) tt) vType -- TODO abstract this out?

412 |     pure (ESome fc t, VOptional (fcToVFC fc) tt)

413 |   infer cxt (ENone fc) =

414 |     pure $ (ENone fc, VHPi (fcToVFC fc) "a" vType $ \a => pure $ (VOptional (fcToVFC fc) a))

415 |   infer cxt e@(EEquivalent fc t u) = do

416 |     (t, tt) <- infer cxt t

417 |     _ <- check cxt u tt

418 |     -- conv (values cxt) tt vType TODO

419 |     pure (e, vType)

420 |   infer cxt (EAssert fc (EEquivalent fc' a b)) = do

421 |     (a, aa) <- infer cxt a

422 |     av <- eval (values cxt) a

423 |     bv <- eval (values cxt) b

424 |     conv (values cxt) av bv

425 |     pure (EAssert fc (EEquivalent fc' a b), VEquivalent (fcToVFC fc') av bv)

426 |   infer cxt (EAssert fc _) = Left $ AssertError fc "not an EEquivalent type" -- TODO better error message

427 |   infer cxt (ERecord fc x) = do

428 |     xs' <- traverse (inferSkip cxt) x

429 |     pure $ (ERecord fc x, VConst (fcToVFC fc) (getHighestType xs'))

430 |   infer cxt (ERecordLit fc x) = do

431 |     xs' <- traverse (inferSkip cxt) x

432 |     pure $ (ERecordLit fc x, VRecord (fcToVFC fc) xs')

433 |   infer cxt (EUnion fc x) = do

434 |     xs' <- traverse (mapMaybe (inferSkip cxt)) x

435 |     pure $ (EUnion fc x, VConst (fcToVFC fc) (getHighestTypeM xs'))

436 |   infer cxt (ECombine fc t u) = do

437 |     (t, tt) <- infer cxt t

438 |     (u, uu) <- infer cxt u

439 |     case (tt, uu) of

440 |          (VRecord _ a', VRecord _ b') => do

441 |            ty <- mergeWithApp (doCombine fc) a' b'

442 |            pure $ (ECombine fc t u, VRecord (fcToVFC fc) ty)

443 |          (VRecord _ _, other) => unexpected "Not a RecordLit" other

444 |          (other, _) => unexpected "Not a RecordLit" other

445 |   infer cxt (ECombineTypes fc a b) = do -- TODO lot of traversals here

446 |     av <- eval (values cxt) a

447 |     bv <- eval (values cxt) b

448 |     case (av, bv) of

449 |          (VRecord _ a', VRecord _ b') => do

450 |            ty <- mergeWithApp (doCombine (fcToVFC fc)) a' b'

451 |            pure $ (ECombineTypes fc a b, snd !(infer cxt !(quote (envNames $ values cxt) (VRecord (fcToVFC fc) ty))))

452 |          (other, _) => unexpected "Not a Record" other

453 |   infer cxt (EPrefer fc t u) = do

454 |     (t, tt) <- infer cxt t

455 |     (u, uu) <- infer cxt u

456 |     case (tt, uu) of

457 |          (VRecord _ a', VRecord _ b') => do

458 |            ty <- mergeWithApp' (doCombine (fcToVFC fc)) a' b'

459 |            pure $ (EPrefer fc t u, VRecord (fcToVFC fc) ty)

460 |          (VRecord _ _, other) => unexpected "Not a RecordLit" other

461 |          (other, _) => unexpected "Not a RecordLit" other

462 |   infer cxt (EMerge fc t u a) = do

463 |     (u, ut) <- infer cxt u

464 |     (t, tt) <- infer cxt t

465 |     case (ut, tt) of

466 |          (VUnion _ ts, VRecord _ us) => do

467 |            case a of

468 |                 Nothing => do

469 |                   pure (EMerge fc t u a, !(inferMerge fc cxt ts us Nothing))

470 |                 (Just a') => do

471 |                   av <- eval (values cxt) a'

472 |                   ty <- inferMerge fc cxt ts us (Just av)

473 |                   conv (values cxt) av ty

474 |                   pure (EMerge fc t u a, av)

475 |          (VOptional _ a', VRecord _ us) =>

476 |            let newUnion = SortedMap.fromList $

477 |                             [(MkFieldName "None", Nothing), (MkFieldName "Some", Just a')]

478 |            in pure (EMerge fc t u a, !(inferMerge (fcToVFC fc) cxt newUnion us Nothing))

479 |          (other, VRecord _ _) => unexpected "Not a RecordLit or Optional" other

480 |          (_, other) => unexpected "Not a RecordLit" other

481 |   infer cxt (EToMap fc t a) = do

482 |     (t, tt) <- infer cxt t

483 |     case tt of

484 |          (VRecord _ ms) =>

485 |            let xs = SortedMap.toList ms in

486 |            case (xs, a) of

487 |                 (((k, v) :: ys), Just x) => do

488 |                   _ <- unifyAllValues cxt v ys

489 |                   _ <- unify cxt (toMapTy v) !(eval (values cxt) x)

490 |                   pure (EToMap fc t a, toMapTy v)

491 |                 (((k, v) :: ys), Nothing) => do

492 |                   _ <- unifyAllValues cxt v ys

493 |                   pure (EToMap fc t a, toMapTy v)

494 |                 ([], Just x) => do v <- checkToMapAnnot cxt !(eval (values cxt) x)

495 |                                    pure (EToMap fc t a, v)

496 |                 ([], Nothing) => Left $ ToMapEmpty fc "Needs an annotation"

497 |          other => unexpected "Not a RecordLit" other

498 |   where

499 |     unifyAllValues : Cxt -> Value -> List (FieldName, Value) -> Either Error Value

500 |     unifyAllValues cxt v vs = do

501 |       unify cxt !(inferSkip cxt !(quote (envNames $ values cxt) v)) (VConst initFC CType)

502 |       _ <- foldlM (\x,y => unify cxt x y *> pure x) v (map snd vs)

503 |       pure v

504 |     checkToMapAnnot : Cxt -> Value -> Either Error Value

505 |     checkToMapAnnot cxt v@(VList fc (VRecord fc' ms)) =

506 |       case SortedMap.toList ms of

507 |            (((MkFieldName "mapKey"), VText initFC) :: ((MkFieldName "mapValue"), a) :: []) => do

508 |              _ <- checkTy cxt !(quote (envNames $ values cxt) a)

509 |              pure v

510 |            other => Left $ ToMapError fc $ "wrong annotation type" ++ show other

511 |     checkToMapAnnot cxt other = Left $ ToMapError (getFC other) $ "wrong annotation type: " ++ show other

512 |   infer cxt (EField fc t k) = do

513 |     (t, tt) <- infer cxt t

514 |     case tt of

515 |          (VConst _ _) =>

516 |             case !(eval (values cxt) t) of

517 |                  VUnion _ ts =>

518 |                     case lookup k ts of

519 |                          (Just Nothing) => pure $ (EField fc t k, VUnion fc ts)

520 |                          (Just (Just a)) => pure $ (EField fc t k, vFun a (VUnion fc ts))

521 |                          Nothing => Left $ FieldNotFoundError fc $ show k

522 |                  x => Left (InvalidFieldType fc (show t))

523 |          (VRecord _ ts) =>

524 |             case lookup k ts of

525 |                  (Just a) => pure $ (EField fc t k, a)

526 |                  Nothing => Left $ FieldNotFoundError fc $ show k

527 |          _ => Left (InvalidFieldType fc (show t))

528 |   infer cxt (ERecordCompletion fc t u) = do

529 |     (t, tt) <- infer cxt t

530 |     case tt of

531 |          (VRecord _ ms) => do

532 |            -- guard $ mapErr "Type" (go (MkFieldName "Type") ms)

533 |            -- guard $ mapErr "default" (go (MkFieldName "default") ms)

534 |            case (lookup (MkFieldName "Type") ms, lookup (MkFieldName "default") ms) of

535 |                 (Just x, Just y) =>

536 |                   infer cxt (EAnnot fc (EPrefer fc (EField fc t (MkFieldName "default")) u) (EField fc t (MkFieldName "Type")))

537 |                 (other, (Just _)) => Left $ InvalidRecordCompletion fc "Type"

538 |                 (_, other) => Left $ InvalidRecordCompletion fc "default"

539 |          other => unexpected "Not a RecordLit" other

540 |   infer cxt (EProject fc t (Left ks)) = do

541 |     (t, tt) <- infer cxt t

542 |     case tt of

543 |          (VRecord _ ms) =>

544 |            pure (EProject fc t (Left ks), VRecord fc $ fromList !(vProjectByFields fc ms ks))

545 |          (other) => unexpected "Not a RecordLit" other

546 |   infer cxt (EProject fc t (Right a)) = do

547 |     (t, tt) <- infer cxt t

548 |     av <- eval (values cxt) a

549 |     case (tt, av) of

550 |          (VRecord _ ms, VRecord _ ms') => do

551 |            pure (EProject fc t (Right a), VRecord fc $ fromList !(vProjectByFields fc ms (keys ms')))

552 |          (other, VRecord _ _) => unexpected "Not a RecordLit" other

553 |          (_, other) => unexpected "Not a Record" other

554 |   infer cxt (EWith fc t ks u) = do -- TODO understand this

555 |     (t, tt) <- infer cxt t

556 |     pure (EWith fc t ks u, !(inferWith tt ks u))

557 |   where

558 |     inferWith : Value -> List1 FieldName -> Expr Void -> Either Error Value

559 |     inferWith (VRecord fc ms) ks y =

560 |       case ks of

561 |            (head ::: []) => do

562 |              (u, uu) <- infer cxt u

563 |              pure $ VRecord fc $ insert head uu ms

564 |            (head ::: (k :: ks)) => do

565 |              let v = case lookup head ms of

566 |                       Nothing => VRecord fc (fromList [])

567 |                       (Just v) => v

568 |              v' <- inferWith v (k ::: ks) y

569 |              pure $ VRecord fc $ insert head v' ms

570 |     inferWith other _ _ = unexpected "Not a RecordLit" other

571 |   infer cxt (EImportAlt fc x y) = infer cxt x

572 |   infer cxt (EEmbed fc (Raw x)) = absurd x

573 |   infer cxt (EEmbed fc (Resolved x)) = infer initCxt x

575 |   toMapTy : Value -> Value

576 |   toMapTy v = VList initFC $ VRecord initFC $ fromList [(MkFieldName "mapKey", VText initFC), (MkFieldName "mapValue", v)]

578 |   checkEmptyMerge : FC -> Maybe Value -> Either Error Value

579 |   checkEmptyMerge fc Nothing = Left $ EmptyMerge fc "Needs a type annotation"

580 |   checkEmptyMerge fc (Just v) = pure v

582 |   inferMerge : FC

583 |              -> Cxt

584 |              -> SortedMap FieldName (Maybe Value)

585 |              -> SortedMap FieldName Value

586 |              -> Maybe Value

587 |              -> Either Error Value

588 |   inferMerge fc cxt us rs mv = do

589 |     xs <- inferUnionHandlers fc (toList us) (toList rs)

590 |     case toList1' xs of

591 |          Nothing => checkEmptyMerge fc mv

592 |          (Just (head ::: tail)) =>

593 |            foldlM (\acc,v => unify cxt acc v *> pure acc) head tail

594 |   where

595 |     checkKeys : FieldName -> FieldName -> Either Error ()

596 |     checkKeys k k' = case k == k' of

597 |                           True => pure ()

598 |                           False => Left $ MergeUnhandledCase fc $ show k

600 |     -- Check there's a 1 to 1 relation between union and handlers.  Relying on

601 |     -- calling this with lists create by `SortedMap.toList` Returns a list of

602 |     -- the types when each handler is applied to the corresponding union

603 |     -- alternative.

604 |     inferUnionHandlers : FC

605 |                       -> List (FieldName, (Maybe Value))

606 |                       -> List (FieldName, Value)

607 |                       -> Either Error (List (Value))

608 |     inferUnionHandlers fc [] [] = pure []

609 |     inferUnionHandlers fc [] ((k, v) :: xs) = Left $ MergeUnusedHandler (getFC v) $ show k

610 |     inferUnionHandlers fc ((k, v) :: xs) [] = Left $ MergeUnhandledCase fc $ show k

611 |     inferUnionHandlers fc ((k, Just v) :: xs) ((k', v') :: ys) = do

612 |       -- if it's an Union field with a value, apply the Record function

613 |       checkKeys k k'

614 |       (_, a', b) <- vAnyPi v'

615 |       unify cxt v a'

616 |       pure $ !(b v) :: !(inferUnionHandlers fc xs ys)

617 |     inferUnionHandlers fc ((k, Nothing) :: xs) ((k', v') :: ys) = do

618 |       -- if it's an Union field without value, return the Record value

619 |       checkKeys k k'

620 |       pure $ v' :: !(inferUnionHandlers fc xs ys)

622 |   ||| infer but only return `Value`, not `(Expr Void, Value)`

623 |   inferSkip : Cxt -> Expr Void -> Either Error Value

624 |   inferSkip cxt = (\e => pure $ snd !(infer cxt e))

626 |   pickHigherType : (acc : U) -> Ty -> U

627 |   pickHigherType CType (VConst _ Kind) = Kind

628 |   pickHigherType _ (VConst _ Sort) = Sort

629 |   pickHigherType acc other = acc

631 |   getHighestTypeM : Foldable t => t (Maybe Value) -> U

632 |   getHighestTypeM x = foldl go CType x

633 |   where

634 |     go : U -> Maybe Value -> U

635 |     go x Nothing = x

636 |     go x (Just y) = pickHigherType x y

638 |   export

639 |   getHighestType : Foldable t => t Value -> U

640 |   getHighestType x = foldl pickHigherType CType x