0 | module Idrall.Eval

  2 | import Idrall.Expr

  3 | import Idrall.Error

  4 | import Idrall.Value

  5 | import Idrall.Map

  7 | import Data.List

  8 | import Data.List1

  9 | import Data.String

 12 | nestError : Either Error b -> Error -> Either Error b

 13 | nestError x e =

 14 |   case x of

 15 |        (Left e') => Left $ NestedError (getFC e') e e'

 16 |        (Right x') => pure x'

 20 | vType : Value

 21 | vType = VConst initFC CType

 25 | vKind : Value

 26 | vKind = VConst initFC Kind

 30 | vSort : Value

 31 | vSort = VConst initFC Sort

 35 |   export

 36 |   inst : Closure -> Value -> Either Error Value

 37 |   inst = evalClosure

 39 |   export

 40 |   covering

 41 |   evalClosure : Closure -> Value -> Either Error Value

 42 |   evalClosure (MkClosure x env e) v

 43 |     = do eval (Extend env x v) e

 45 |   evalVar : FC -> Env -> Name -> Int -> Either Error Value

 46 |   evalVar fc Empty x i = pure $ VVar fc x (0 - i - 1)

 47 |   evalVar fc (Skip env x') x i =

 48 |     case x == x' of

 49 |          True => if i == 0 then pure $ VVar fc x (countName x env) else evalVar fc env x (i - 1)

 50 |          False => evalVar fc env x i

 51 |   evalVar fc (Extend env x' v) x i =

 52 |     case x == x' of

 53 |          True => if i == 0 then pure v else evalVar fc env x (i - 1)

 54 |          False => evalVar fc env x i

 61 |   export

 62 |   covering

 63 |   eval : Env -> Expr Void -> Either Error Value

 64 |   eval env (EConst fc x) = pure (VConst fc x)

 65 |   eval env (EVar fc x i)

 66 |     = evalVar fc env x i

 67 |   eval env (ELam fc x ty body)

 68 |     = do vTy <- eval env ty

 69 |          pure (VLambda fc vTy (MkClosure x env body))

 70 |   eval env (EPi fc x dom ran)

 71 |     = do ty <- eval env dom

 72 |          pure (VPi fc ty (MkClosure x env ran))

 73 |   eval env (EApp fc rator rand)

 74 |     = do rator' <- eval env rator

 75 |          rand' <- eval env rand

 76 |          doApply rator' rand'

 77 |   eval env (ELet fc x _ r e) =

 78 |     do vr <- eval env r

 79 |        eval (Extend env x vr) e

 80 |   eval env (EAnnot fc x _) = eval env x

 81 |   eval env (EBool fc) = pure $ VBool fc

 82 |   eval env (EBoolLit fc b) = pure $ VBoolLit fc b

 83 |   eval env (EBoolAnd fc t u) =

 84 |     case (!(eval env t), !(eval env u)) of

 85 |          (VBoolLit _ True, u) => pure u

 86 |          (VBoolLit _ False, u) => pure $ VBoolLit fc False

 87 |          (t, VBoolLit _ True) => pure t

 88 |          (t, VBoolLit _ False) => pure $ VBoolLit fc False

 89 |          (t, u) => case conv env t u of

 90 |                         Right _ => pure t

 91 |                         Left _ => pure $ VBoolAnd fc t u

 92 |   eval env (EBoolOr fc t u) =

 93 |     case (!(eval env t), !(eval env u)) of

 94 |          (VBoolLit _ False, u) => pure u

 95 |          (VBoolLit _ True, u) => pure $ VBoolLit fc True

 96 |          (t, VBoolLit _ False) => pure t

 97 |          (t, VBoolLit _ True) => pure $ VBoolLit fc True

 98 |          (t, u) => case conv env t u of

 99 |                         Right _ => pure t

100 |                         Left _ => pure $ VBoolOr fc t u

101 |   eval env (EBoolEQ fc t u) =

102 |     case (!(eval env t), !(eval env u)) of

103 |          (VBoolLit _ True, u) => pure u

104 |          (t, VBoolLit _ True) => pure t

105 |          (t, u) => case conv env t u of

106 |                         Right _ => pure $ VBoolLit fc True

107 |                         Left _ => pure $ VBoolEQ fc t u

108 |   eval env (EBoolNE fc t u) =

109 |     case (!(eval env t), !(eval env u)) of

110 |          (VBoolLit _ False, u) => pure u

111 |          (t, VBoolLit _ False) => pure t

112 |          (t, u) => case conv env t u of

113 |                         Right _ => pure $ VBoolLit fc False

114 |                         Left _ => pure $ VBoolNE fc t u

115 |   eval env (ENatural fc) = pure $ VNatural fc

116 |   eval env (ENaturalLit fc k) = pure $ VNaturalLit fc k

117 |   eval env (ENaturalBuild fc) =

118 |     pure $ VPrim $

119 |       \c => case c of

120 |                  VPrimVar fc => pure $ VNaturalBuild fc $ VPrimVar fc

121 |                  t => vAppM t [ VNatural fc

122 |                               , VHLam fc (Typed "n" $ VNatural fc) $ \n =>

123 |                                     pure $ vNaturalPlus fc n (VNaturalLit fc 1)

124 |                               , VNaturalLit fc 0

125 |                               ]

126 |   eval env (ENaturalFold fc) =

127 |     pure $ VPrim $ \n =>

128 |     pure $ VPrim $ \natural =>

129 |     pure $ VPrim $ \succ =>

130 |     pure $ VPrim $ \zero =>

131 |     let inert = VNaturalFold (fcToVFC fc) n natural succ zero

132 |     in case zero of

133 |             VPrimVar _ => pure inert

134 |             _ => case succ of

135 |                       VPrimVar _ => pure inert

136 |                       _ => case natural of

137 |                                 VPrimVar _ => pure inert

138 |                                 _ => case n of

139 |                                           VNaturalLit _ n' =>

140 |                                               go succ zero n'

141 |                                           _ => pure inert

142 |   where

143 |     go : Value -> Value -> Nat -> Either Error Value

144 |     go succ acc 0 = pure acc

145 |     go succ acc (S k) = go succ !(vApp succ acc) k

146 |   eval env (ENaturalIsZero fc) =

147 |      pure $ VPrim $

148 |        \c => case c of

149 |                   VNaturalLit fc' n => pure $ VBoolLit fc' (n == 0)

150 |                   n             => pure $ VNaturalIsZero fc n

151 |   eval env (EBoolIf fc b t f) =

152 |     case (!(eval env b), !(eval env t), !(eval env f)) of

153 |          (VBoolLit _ True, t, f) => pure t

154 |          (VBoolLit _ False, t, f) => pure f

155 |          (b, VBoolLit _ True, VBoolLit _ False) => pure b

156 |          (b, t, f) => case conv env t f of

157 |                            (Right _) => pure t

158 |                            (Left _) => pure $ VBoolIf fc b t f

159 |   eval env (ENaturalEven fc) =

160 |     pure $ VPrim $

161 |       \c => case c of

162 |                  VNaturalLit fc n => pure $ VBoolLit fc (isEven n)

163 |                  n             => pure $ VNaturalEven fc n

164 |   eval env (ENaturalOdd fc) =

165 |     pure $ VPrim $

166 |       \c => case c of

167 |                  VNaturalLit fc n => pure $ VBoolLit fc (isOdd n)

168 |                  n             => pure $ VNaturalOdd fc n

169 |   eval env (ENaturalSubtract fc) = do

170 |     pure $ VPrim $

171 |       \x => case x of

172 |                  VNaturalLit fc 0 => pure $ VHLam fc NaturalSubtractZero (\y => pure y)

173 |                  x'@(VNaturalLit fc m) => pure $ VPrim $

174 |                       \y => case y of

175 |                                  -- unintuitive order for `minus`, but this is correct

176 |                                  (VNaturalLit fc n) => pure $ VNaturalLit fc (minus n m)

177 |                                  y' => pure $ VNaturalSubtract fc x' y'

178 |                  x' => pure $ VPrim $

179 |                       \y => case y of

180 |                                  (VNaturalLit fc 0) => pure $ VNaturalLit fc 0

181 |                                  y' => case conv env x' y' of

182 |                                             (Right _) => pure $ VNaturalLit fc 0

183 |                                             (Left _) => pure $ VNaturalSubtract fc x' y'

184 |   eval env (ENaturalShow fc) =

185 |     pure $ VPrim $

186 |       \c => case c of

187 |                  VNaturalLit fc n => pure $ VTextLit fc (MkVChunks [] (show n))

188 |                  n             => pure $ VNaturalShow fc n

189 |   eval env (ENaturalToInteger fc) =

190 |     pure $ VPrim $

191 |       \c => case c of

192 |                  VNaturalLit fc n => pure $ VIntegerLit fc (cast n)

193 |                  n             => pure $ VNaturalToInteger fc n

194 |   eval env (ENaturalPlus fc t u) = pure $ vNaturalPlus fc !(eval env t) !(eval env u)

195 |   eval env (ENaturalTimes fc t u) =

196 |     case (!(eval env t), !(eval env u)) of

197 |          (VNaturalLit _ 0, u) => pure $ VNaturalLit fc 0

198 |          (VNaturalLit _ 1, u) => pure u

199 |          (t, VNaturalLit _ 1) => pure t

200 |          (t, VNaturalLit _ 0) => pure $ VNaturalLit fc 0

201 |          (VNaturalLit _ t, VNaturalLit _ u) => pure (VNaturalLit fc $ t * u)

202 |          (t, u) => pure $ VNaturalTimes fc t u

203 |   eval env (EInteger fc) = pure $ VInteger fc

204 |   eval env (EIntegerLit fc k) = pure (VIntegerLit fc k)

205 |   eval env (EIntegerShow fc) =

206 |     pure $ VPrim $

207 |       \c => case c of

208 |                  VIntegerLit fc n => case n >= 0 of

209 |                                        True => pure $ VTextLit fc (MkVChunks [] ("+" ++ (show n)))

210 |                                        False => pure $ VTextLit fc (MkVChunks [] (show n))

211 |                  n             => pure $ VIntegerShow fc n

212 |   eval env (EIntegerNegate fc) = pure $ VPrim $

213 |                             \c => case c of

214 |                                        VIntegerLit fc n => pure $ VIntegerLit fc (negate n)

215 |                                        n             => pure $ VIntegerNegate fc n

216 |   eval env (EIntegerClamp fc) =

217 |     pure $ VPrim $

218 |       \c => case c of

219 |                  VIntegerLit fc n => pure $ VNaturalLit fc (integerToNat n)

220 |                  n             => pure $ VIntegerClamp fc n

221 |   eval env (EIntegerToDouble fc) =

222 |     pure $ VPrim $

223 |       \c => case c of

224 |                  VIntegerLit fc n => pure $ VDoubleLit fc (cast n)

225 |                  n             => pure $ VIntegerToDouble fc n

226 |   eval env (EDouble fc) = pure $ VDouble fc

227 |   eval env (EDoubleLit fc k) = pure (VDoubleLit fc k)

228 |   eval env (EDoubleShow fc) =

229 |     pure $ VPrim $

230 |       \c => case c of

231 |                  VDoubleLit fc n => pure $ VTextLit fc (MkVChunks [] (show n))

232 |                  n             => pure $ VDoubleShow fc n

233 |   eval env (EText fc) = pure $ VText fc

234 |   eval env (ETextLit fc (MkChunks xs x)) = do

235 |     xs' <- traverse (mapChunks (eval env)) xs

236 |     let xs'' = compressChunks xs'

237 |     case (xs'', x) of

238 |          ([("", t)], "") => pure t

239 |          _ => pure (VTextLit fc (MkVChunks xs'' x))

240 |   eval env (ETextAppend fc x y) =

241 |     case (!(eval env x), !(eval env y)) of

242 |          (VTextLit fc (MkVChunks [] ""), u) => pure u

243 |          (t, VTextLit fc (MkVChunks [] "")) => pure t

244 |          (VTextLit fc x, VTextLit fc' y) => pure $ VTextLit fc (x <+> y)

245 |          (t, u) => pure $ VTextAppend fc t u

246 |   eval env (ETextShow fc) =

247 |     pure $ VPrim $ \c =>

248 |       case c of

249 |            VTextLit fc (MkVChunks [] x) => pure $ VTextLit fc (MkVChunks [] (vTextShow x))

250 |            t => pure $ VTextShow fc t

251 |   eval env (ETextReplace fc) = -- Probably not right

252 |     pure $ VPrim $

253 |       \needle => pure $ VPrim $

254 |         \replacement => pure $ VPrim $

255 |           \haystack =>

256 |             case needle of

257 |                  VTextLit fc (MkVChunks [] "") => pure haystack

258 |                  VTextLit fc (MkVChunks [] needleText) =>

259 |                    case haystack of

260 |                         (VTextLit fc (MkVChunks [] haystackText)) =>

261 |                           case replacement of

262 |                                (VTextLit fc (MkVChunks [] replacementText)) =>

263 |                                  pure $ VTextLit fc $

264 |                                         MkVChunks [] $ textReplace needleText replacementText haystackText

265 |                                (VTextLit fc (MkVChunks chx replacementText)) =>

266 |                                  case strFromChunks chx  of

267 |                                       Nothing => Left $ ErrorMessage fc "could not make string for replacement"

268 |                                       (Just str) =>

269 |                                          pure $ VTextLit fc $

270 |                                          MkVChunks [] $ textReplace

271 |                                                           needleText

272 |                                                           replacementText

273 |                                                           haystackText

274 |                                _ => pure $ VTextReplace fc needle replacement haystack

275 |                         _ => pure $ VTextReplace fc needle replacement haystack

276 |                  k => pure $ VTextReplace fc needle replacement haystack

277 |   eval env (EList fc) = do

278 |     pure $ VPrim $ \a => pure $ VList fc a

279 |   eval env (EListLit fc Nothing es) = do

280 |     vs <- mapListEither es (eval env)

281 |     pure (VListLit fc Nothing vs)

282 |   eval env (EListLit fc (Just ty) es) = do

283 |     ty' <- eval env ty

284 |     vs <- mapListEither es (eval env)

285 |     pure (VListLit fc (Just ty') vs)

286 |   eval env (EListAppend fc x y) = do

287 |     x' <- eval env x

288 |     y' <- eval env y

289 |     vListAppend fc x' y'

290 |   eval env (EListBuild fc) =

291 |     pure $ VPrim $

292 |       \a => pure $ VPrim $

293 |         \c => case c of

294 |                    VPrimVar fc => pure $ VListBuild fc a $ VPrimVar fc

295 |                    t => vAppM t [ VList fc a

296 |                                 , VHLam fc (Typed "a" a) $ \x =>

297 |                                     pure $ VHLam fc (Typed "as" (VList fc a)) $ \as =>

298 |                                       vListAppend fc (VListLit fc Nothing [x]) as

299 |                                 , VListLit fc (Just a) []

300 |                                 ]

301 |   eval env (EListFold fc) =

302 |     pure $ VPrim $ \a =>

303 |     pure $ VPrim $ \as =>

304 |     pure $ VPrim $ \list =>

305 |     pure $ VPrim $ \cons =>

306 |     pure $ VPrim $ \nil =>

307 |       let inert = pure $ VListFold fc a as list cons nil in

308 |         case nil of

309 |         VPrimVar fc => inert

310 |         _ => case cons of

311 |             VPrimVar fc => inert

312 |             _ => case list of

313 |                 VPrimVar fc => inert

314 |                 _ => case a of

315 |                     VPrimVar fc => inert

316 |                     _ => case as of

317 |                         VListLit fc _ as' =>

318 |                            foldrM (\x,b => vAppM cons [x, b]) nil as'

319 |                         _ => inert

320 |     where

321 |       foldrM : (Foldable t, Monad m) => (funcM: b -> a -> m a) -> (init: a) -> (input: t b) -> m a

322 |       foldrM fm a0 = foldr (\b,ma => ma >>= fm b) (pure a0)

323 |   eval env (EListLength fc) =

324 |     pure $ VPrim $

325 |       \a => pure $ VPrim $

326 |         \c => case c of

327 |                    (VListLit fc _ as) => pure $ VNaturalLit fc (length as)

328 |                    as => pure $ VListLength fc a as

329 |   eval env (EListHead fc) =

330 |     pure $ VPrim $ \a =>

331 |       pure $ VPrim $

332 |              \c => case c of

333 |                         VListLit fc _ [] => pure $ VNone fc a

334 |                         VListLit fc _ (h :: _) => pure $ VSome fc h

335 |                         as => pure $ VListHead fc a as

336 |   eval env (EListLast fc) =

337 |     pure $ VPrim $

338 |       \a => pure $ VPrim $

339 |         \c => case c of

340 |                    VListLit fc _ as =>

341 |                      case last' as of

342 |                           Nothing => pure $ VNone fc a

343 |                           (Just t) => pure $ VSome fc t

344 |                    as => pure $ VListLast fc a as

345 |   eval env (EListIndexed fc) =

346 |     pure $ VPrim $

347 |       \a => pure $ VPrim $

348 |         \c => case c of

349 |                    VListLit fc t as => pure $ vListIndexed fc t as

350 |                    as => pure $ VListLast fc a as

351 |   eval env (EListReverse fc) =

352 |     pure $ VPrim $

353 |       \a => pure $ VPrim $

354 |         \c => case c of

355 |                    VListLit fc t as => pure $ VListLit fc t (reverse as)

356 |                    as => pure $ VListReverse fc a as

357 |   eval env (EOptional fc) = pure $ VPrim $ \a => pure $ VOptional fc a

358 |   eval env (ESome fc a) = pure (VSome fc !(eval env a))

359 |   eval env (ENone fc) = pure $ VPrim $ \a => pure $ VNone fc a

360 |   eval env (EEquivalent fc x y) =

361 |     do xV <- eval env x

362 |        yV <- eval env y

363 |        pure (VEquivalent fc xV yV)

364 |   eval env (EAssert fc x) = do

365 |     xV <- eval env x

366 |     doAssert env xV

367 |   eval env (ERecord fc x) =

368 |     let xs = toList x in

369 |     do xs' <- traverse (mapRecord (eval env)) xs

370 |        pure (VRecord fc (fromList xs'))

371 |   eval env (ERecordLit fc x) =

372 |     let xs = toList x in

373 |     do xs' <- traverse (mapRecord (eval env)) xs

374 |        pure (VRecordLit fc (fromList xs'))

375 |   eval env (ECombine fc x y) = do

376 |     x' <- eval env x

377 |     y' <- eval env y

378 |     doCombine fc x' y'

379 |   eval env (ECombineTypes fc x y) = do

380 |     x' <- eval env x

381 |     y' <- eval env y

382 |     doCombine fc x' y'

383 |   eval env (EPrefer fc x y) = do

384 |     x' <- eval env x

385 |     y' <- eval env y

386 |     doPrefer fc x' y'

387 |   eval env (EMerge fc x y ma) = -- TODO Double check this

388 |     case (!(eval env x), !(eval env y), !(mapMaybe (eval env) ma)) of

389 |          (VRecordLit fc m, VInject fc' _ k (Just t), _) =>

390 |            case lookup k m of

391 |                 Just f => vApp f t

392 |                 Nothing => Left $ MergeUnhandledCase fc $ show k -- TODO DRY these error conditions

393 |          (VRecordLit fc m, VInject fc' _ k _, _) =>

394 |            case lookup k m of

395 |                 Just t => pure t

396 |                 Nothing => Left $ MergeUnhandledCase fc $ show k

397 |          (VRecordLit fc m, VSome fc' t, _) =>

398 |            case lookup (MkFieldName "Some") m of

399 |                 Just f => vApp f t

400 |                 Nothing => Left $ MergeUnhandledCase fc $ "Some"

401 |          (VRecordLit fc m, VNone fc' _, _) =>

402 |            case lookup (MkFieldName "None") m of

403 |                 Just t => pure t

404 |                 Nothing => Left $ MergeUnhandledCase fc $ "None"

405 |          (t, u, ma) => pure $ VMerge fc t u ma

406 |   eval env (EUnion fc x) =

407 |     let xs = toList x in

408 |     do xs' <- traverse (mapUnion (eval env)) xs

409 |        pure (VUnion fc (fromList xs'))

410 |   eval env (EField fc x k) =

411 |     case !(eval env x) of

412 |          VRecordLit fc m =>

413 |             case lookup k m of

414 |                  (Just v) => pure v

415 |                  Nothing => Left (FieldNotFoundError fc $ show k)

416 |          VUnion fc m =>

417 |             case lookup k m of

418 |                  (Just (Just y)) => pure $ VPrim $ \u => pure $ VInject fc m k (Just u)

419 |                  (Just Nothing) => pure $ VInject fc m k Nothing

420 |                  Nothing => Left (FieldNotFoundError fc $ show k)

421 |          t => pure $ VField fc t k

422 |   eval env (ERecordCompletion fc t u) =

423 |     eval env (EAnnot fc (EPrefer fc (EField fc t (MkFieldName "default")) u) (EField fc t (MkFieldName "Type")))

424 |   eval env (EToMap fc x Nothing) =

425 |     case !(eval env x) of

426 |          VRecordLit fc ms =>

427 |            let xs = SortedMap.toList ms in

428 |                case xs of

429 |                     [] => Left $ ToMapEmpty fc "Needs an annotation"

430 |                     (y :: ys) => pure $ VListLit fc Nothing $ map vToMap (y :: ys)

431 |          other => pure $ VToMap fc other Nothing

432 |   eval env (EToMap fc x (Just y)) = do

433 |     y' <- eval env y

434 |     case !(eval env x) of

435 |          VRecordLit fc ms => pure $ VListLit fc (Just y') $ map vToMap (SortedMap.toList ms)

436 |          other => pure $ VToMap fc other Nothing

437 |   eval env (EProject fc x (Left ks)) =

438 |     case !(eval env x) of

439 |          VRecordLit fc ms => pure $ VRecordLit fc $ fromList !(vProjectByFields fc ms ks)

440 |          other => Left (Unexpected fc $ "Not a RecordLit. Value: " ++ show other)

441 |   eval env (EProject fc x (Right y)) =

442 |     case (!(eval env x), !(eval env y)) of

443 |          (VRecordLit fc ms, VRecordLit fc' ms') => pure $ VRecordLit fc $ fromList !(vProjectByFields fc ms (keys ms'))

444 |          (other, VRecord fc _) => Left (Unexpected fc $ "Not a RecordLit. Value: " ++ show other)

445 |          (_, other) => Left (Unexpected fc $ "Not a Record. Value: " ++ show other)

446 |   eval env (EWith fc x ks y) = vWith fc !(eval env x) ks !(eval env y)

447 |   eval env (EImportAlt fc x y) = eval env x

448 |   eval env (EEmbed fc (Raw x)) = absurd x

449 |   eval env (EEmbed fc (Resolved x)) = eval Empty x

451 |   vTextShow : String -> String

452 |   vTextShow x = "\"" <+> (foldl (<+>) "" (map f (unpack x))) <+> "\""

453 |   where

454 |     f : Char -> String

455 |     f '"'  = "\\\""

456 |     f '$'  = "\\u0024"

457 |     f '\\' = "\\\\"

458 |     f '\b' = "\\b"

459 |     f '\n' = "\\n"

460 |     f '\r' = "\\r"

461 |     f '\t' = "\\t"

462 |     f '\f' = "\\f"

463 |     -- TODO handle this case

464 |     -- https://github.com/dhall-lang/dhall-haskell/blob/f33e8cff8fc51e4a562f48fcf987e6af5e09142d/dhall/src/Dhall/Eval.hs#L847

465 |     f c = case c <= '\x1F' of

466 |                True => singleton c

467 |                False => singleton c

469 |   vToMap : (FieldName, Value) -> Value

470 |   vToMap (MkFieldName k, v) = VRecordLit initFC $ fromList

471 |     [ (MkFieldName "mapKey", VTextLit initFC $ MkVChunks [] k)

472 |     , (MkFieldName "mapValue", v)

473 |     ]

475 |   vWith : FC -> Value -> List1 FieldName -> Value -> Either Error Value

476 |   vWith _ (VRecordLit fc ms) (head ::: []) u = pure $ VRecordLit fc $ insert head u ms

477 |   vWith _ (VRecordLit fc ms) (head ::: (k :: ks)) u =

478 |     case lookup head ms of

479 |          Nothing =>

480 |            let new = VRecordLit fc (fromList [])

481 |                rest = vWith fc new (k ::: ks) u

482 |            in

483 |            pure $ VRecordLit fc $ insert head !rest ms

484 |          (Just u') =>

485 |            let rest = vWith fc u' (k ::: ks) u in

486 |            pure $ VRecordLit fc $ insert head !rest ms

487 |   vWith fc t ks u = pure $ VWith fc t ks u

489 |   export

490 |   vProjectByFields : FC -> SortedMap FieldName Value -> List FieldName -> Either Error (List (FieldName, Value))

491 |   vProjectByFields fc ms ks = traverse (lookupRecord ms) ks

492 |   where

493 |     lookupRecord : SortedMap FieldName Value -> FieldName -> Either Error (FieldName, Value)

494 |     lookupRecord ms k = case lookup k ms of

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

496 |                              (Just v) => pure (k, v)

498 |   listIndexedType : Maybe Value -> Maybe Value

499 |   listIndexedType Nothing = Nothing

500 |   listIndexedType (Just a) =

501 |     Just $ VRecord initFC (fromList [(MkFieldName "index", VNatural initFC), (MkFieldName "value", a)])

503 |   vNaturalPlus : FC -> Value -> Value -> Value

504 |   vNaturalPlus fc (VNaturalLit _ 0) u = u

505 |   vNaturalPlus fc t (VNaturalLit _ 0) = t

506 |   vNaturalPlus fc (VNaturalLit _ t) (VNaturalLit _ u) = VNaturalLit fc $ t + u

507 |   vNaturalPlus fc t u = VNaturalPlus fc t u

509 |   -- TODO lots of traversals here

510 |   vListIndexed : FC -> Maybe Value -> List Value -> Value

511 |   vListIndexed fc a xs =

512 |     let prep = foldl go [] xs

513 |         lists = map toRecordList prep

514 |         recordsAsLists = map toRecordList prep

515 |         final = map toRecord recordsAsLists

516 |         in VListLit fc (listIndexedType a) (reverse final) -- TODO hacky reverse

517 |   where

518 |     go : List (Nat, Value) -> Value -> List (Nat, Value)

519 |     go [] t = [(0, t)]

520 |     go acc@((i, _) :: _) u = (i+1, u) :: acc

521 |     toRecordList : (Nat, Value) -> List (FieldName, Value)

522 |     toRecordList (i, v) = [(MkFieldName "index", VNaturalLit (fcToVFC $ getFC v) i), (MkFieldName "value", v)]

523 |     toRecord : List (FieldName, Value) -> Value

524 |     toRecord xs = VRecordLit (fcToVFC fc) $ fromList xs

526 |   covering

527 |   doApply : Value -> Value -> Either Error Value

528 |   doApply (VLambda fc ty closure) arg =

529 |     evalClosure closure arg

530 |   doApply (VHLam fc i f) arg = (f arg)

531 |   doApply f arg = pure $ VApp (fcToVFC $ getFC f) f arg

533 |   vApp : Value -> Value -> Either Error Value

534 |   vApp = doApply

536 |   vAppM : Value -> List Value -> Either Error Value

537 |   vAppM x xs = foldlM vApp x xs

539 |   covering

540 |   doAssert : Env -> Value -> Either Error Value

541 |   doAssert env v@(VEquivalent fc t u) = do

542 |     conv env t u

543 |     pure $ VAssert fc v

544 |   doAssert env x = Left (AssertError (getFC x) ("not an equivalence type: " ++ show x))

546 |   vListAppend : FC -> Value -> Value -> Either Error Value

547 |   vListAppend fc (VListLit fc' _ []) u = pure u

548 |   vListAppend fc t (VListLit fc' _ []) = pure t

549 |   vListAppend fc (VListLit fc' t xs) (VListLit fc'' _ ys) =

550 |     pure (VListLit fc t (xs ++ ys))

551 |   vListAppend fc x y = pure $ VListAppend fc x y

553 |   export

554 |   doCombine : FC -> Value -> Value -> Either Error Value

555 |   doCombine _ (VRecordLit fc x) (VRecordLit fc' y) =

556 |     pure (VRecordLit fc $ !(mergeWithApp (doCombine fc) x y))

557 |   doCombine _ (VRecord fc x) (VRecord fc' y) =

558 |     pure (VRecord fc $ !(mergeWithApp (doCombine fc) x y))

559 |   doCombine fc x y = pure $ VCombineTypes fc x y

561 |   doPrefer : FC -> Value -> Value -> Either Error Value

562 |   doPrefer _ (VRecordLit fc x) (VRecordLit fc' y) =

563 |     pure (VRecordLit fc $ !(mergeWithApp' (doPrefer fc) x y))

564 |   doPrefer fc x y = pure $ VPrefer fc x y

566 |   -- conversion checking

567 |   -- Needs to be in mutual block with eval because it's used by Bool builtins

569 |   countName : Name -> Env -> Int

570 |   countName x env = go 0 env

571 |   where

572 |     go : (acc : Int) -> Env -> Int

573 |     go acc Empty = acc

574 |     go acc (Skip env x') = go (if x == x' then acc + 1 else acc) env

575 |     go acc (Extend env x' _) = go (if x == x' then acc + 1 else acc) env

577 |   convFresh : Name -> Env -> (Name, Value)

578 |   convFresh x env = (x, VVar initFC x (countName x env))

580 |   convFreshCl : Closure -> Env -> (Name, Value, Closure)

581 |   convFreshCl cl@(MkClosure x _ _) env = (x, snd (convFresh x env), cl)

583 |   convErr : (Show x) => FC -> x -> x -> Either Error a

584 |   convErr fc x y = Left $ AlphaEquivError fc $ show x ++ "\n not alpha equivalent to:\n" ++ show y

586 |   export

587 |   compressChunks : List (String, Value) -> List (String, Value)

588 |   compressChunks [] = []

589 |   compressChunks (("", (VTextLit _ (MkVChunks [] ""))) :: xs) = compressChunks xs

590 |   compressChunks (x :: xs) = x :: compressChunks xs

592 |   export

593 |   strFromExpr : Expr Void -> Maybe String

594 |   strFromExpr (ETextLit fc (MkChunks [] x)) = pure x

595 |   strFromExpr (ETextLit fc (MkChunks (start :: xs) end)) =

596 |     let mid = traverse go xs in

597 |     pure $ !(go start) ++ (foldl (<+>) "" !mid) ++ end

598 |   where

599 |     go : (String, Expr Void) -> Maybe String

600 |     go (x, e) = pure $ x ++ !(strFromExpr e)

601 |   strFromExpr _ = Nothing

603 |   export

604 |   strFromChunks : List (String, Value) -> Maybe String

605 |   strFromChunks [] = Just neutral

606 |   strFromChunks ((str, (VTextLit _ (MkVChunks xys' y))) :: xs') = do

607 |     rest <- strFromChunks xs'

608 |     mid <- strFromChunks xys'

609 |     Just (str ++ mid ++ y ++ rest)

610 |   strFromChunks ((str, _) :: xs') = Nothing

612 |   convChunks : FC -> Env -> VChunks -> VChunks -> Either Error ()

613 |   convChunks fc env (MkVChunks [] z) (MkVChunks [] z') = convEq fc z z'

614 |   convChunks fc env (MkVChunks ((s, t) :: xys) z) (MkVChunks ((s', t') :: xys') z') = do

615 |     convEq fc s s'

616 |     conv env t t'

617 |     convChunks fc env (MkVChunks xys z) (MkVChunks xys' z')

618 |   convChunks fc env t u = convErr fc t u

620 |   convList : FC -> Env -> List Value -> List Value -> Either Error ()

621 |   convList fc env [] [] = pure ()

622 |   convList fc env (t :: xs) (t' :: xs') = do

623 |     conv env t t'

624 |     convList fc env xs xs'

625 |   convList fc env t u = convErr fc t u

627 |   convUnion : FC -> Env -> List (FieldName, Maybe Value) -> List (FieldName, Maybe Value) -> Either Error ()

628 |   convUnion fc env [] [] = pure ()

629 |   convUnion fc env ((x, Just t) :: xs) ((x', Just t') :: ys) = do

630 |     convEq fc x x'

631 |     conv env t t'

632 |     convUnion fc env xs ys

633 |   convUnion fc env ((x, Nothing) :: xs) ((x', Nothing) :: ys) = do

634 |     convEq fc x x'

635 |     convUnion fc env xs ys

636 |   convUnion fc env t u = convErr fc t u

638 |   convEq : (Eq x, Show x) => FC -> x -> x -> Either Error ()

639 |   convEq fc a b =

640 |     case a == b of

641 |          True => pure ()

642 |          False => convErr fc a b

644 |   convSkip : Env -> Name -> Value -> Value -> Either Error ()

645 |   convSkip env x = conv (Skip env x)

647 |   export

648 |   conv : Env -> Value -> Value -> Either Error ()

649 |   conv env (VLambda fc _ t) (VLambda fc' _ t') =

650 |     let (x, v, t) = convFreshCl t env in do

651 |     convSkip env x !(inst t v) !(inst t' v)

652 |   conv env (VLambda fc _ t) (VHLam fc' _ t') =

653 |     let (x, v, t) = convFreshCl t env in do

654 |     convSkip env x !(inst t v) !(t' v)

655 |   conv env (VLambda fc _ t) t' =

656 |     let (x, v, t) = convFreshCl t env in do

657 |     convSkip env x !(inst t v) !(vApp t' v)

658 |   conv env (VHLam fc _ t) (VLambda fc' _ t') =

659 |     let (x, v, t') = convFreshCl t' env in do

660 |     convSkip env x !(t v) !(inst t' v)

661 |   conv env (VHLam fc _ t) (VHLam fc' _ t') =

662 |     let (x, v) = convFresh "x" env in do

663 |     convSkip env x !(t v) !(t' v)

664 |   conv env (VHLam fc _ t) t' =

665 |     let (x, v) = convFresh "x" env in do

666 |     convSkip env x !(t v) !(vApp t' v)

667 |   conv env t (VLambda fc _ t') =

668 |     let (x, v, t') = convFreshCl t' env in do

669 |     convSkip env x !(vApp t v) !(inst t' v)

670 |   conv env t (VHLam fc _ t') =

671 |     let (x, v) = convFresh "x" env in do

672 |     convSkip env x !(vApp t v) !(t' v)

674 |   conv env (VPi fc a b) (VPi fc' a' b') =

675 |     let (x, v, b') = convFreshCl b' env in do

676 |     conv env a a'

677 |     convSkip env x !(inst b v) !(inst b' v)

678 |   conv env (VPi fc a b) (VHPi fc' x a' b') =

679 |     let (x, v) = convFresh "x" env in do

680 |     conv env a a'

681 |     convSkip env x !(inst b v) !(b' v)

682 |   conv env (VHPi fc _ a b) (VPi fc' a' b') =

683 |     let (x, v, b') = convFreshCl b' env in do

684 |     conv env a a'

685 |     convSkip env x !(b v) !(inst b' v)

686 |   conv env (VHPi fc _ a b) (VHPi fc' x a' b') =

687 |     let (x, v) = convFresh "x" env in do

688 |     conv env a a'

689 |     convSkip env x !(b v) !(b' v)

691 |   conv env (VConst fc k) (VConst fc' k') = convEq fc k k'

692 |   conv env (VVar fc x i) (VVar fc' x' i') = do

693 |     convEq fc x x'

694 |     convEq fc i i'

696 |   conv env (VApp fc t u) (VApp fc' t' u') = do

697 |     conv env t t'

698 |     conv env u u'

699 |   conv env (VBool fc) (VBool fc') = pure ()

700 |   conv env (VBoolLit fc b) (VBoolLit fc' b') = convEq fc b b'

701 |   conv env (VBoolAnd fc t u) (VBoolAnd fc' t' u') = do

702 |     conv env t t'

703 |     conv env u u'

704 |   conv env (VBoolOr fc t u) (VBoolOr fc' t' u') = do

705 |     conv env t t'

706 |     conv env u u'

707 |   conv env (VBoolEQ fc t u) (VBoolEQ fc' t' u') = do

708 |     conv env t t'

709 |     conv env u u'

710 |   conv env (VBoolNE fc t u) (VBoolNE fc' t' u') = do

711 |     conv env t t'

712 |     conv env u u'

713 |   conv env (VBoolIf fc b t f) (VBoolIf fc' b' t' f') = do

714 |     conv env b b'

715 |     conv env t t'

716 |     conv env f f'

717 |   conv env (VNatural fc) (VNatural fc') = pure ()

718 |   conv env (VNaturalLit fc k) (VNaturalLit fc' k') = convEq fc k k'

719 |   conv env (VNaturalBuild fc t) (VNaturalBuild fc' t') = conv env t t'

720 |   conv env (VNaturalFold fc t u v w) (VNaturalFold fc' t' u' v' w') = do

721 |     conv env t t'

722 |     conv env u u'

723 |     conv env v v'

724 |     conv env w w'

725 |   conv env (VNaturalIsZero fc t) (VNaturalIsZero fc' t') = conv env t t'

726 |   conv env (VNaturalEven fc t) (VNaturalEven fc' t') = conv env t t'

727 |   conv env (VNaturalOdd fc t) (VNaturalOdd fc' t') = conv env t t'

728 |   conv env (VNaturalShow fc t) (VNaturalShow fc' t') = conv env t t'

729 |   conv env (VNaturalSubtract fc t u) (VNaturalSubtract fc' t' u') = do

730 |     conv env t t'

731 |     conv env u u'

732 |   conv env (VNaturalToInteger fc t) (VNaturalToInteger fc' t') = conv env t t'

733 |   conv env (VNaturalPlus fc t u) (VNaturalPlus fc' t' u') = do

734 |     conv env t t'

735 |     conv env u u'

736 |   conv env (VNaturalTimes fc t u) (VNaturalTimes fc' t' u') = do

737 |     conv env t t'

738 |     conv env u u'

739 |   conv env (VInteger fc) (VInteger fc') = pure ()

740 |   conv env (VIntegerLit fc t) (VIntegerLit fc' t') = convEq fc t t'

741 |   conv env (VIntegerShow fc t) (VIntegerShow fc' t') = conv env t t'

742 |   conv env (VIntegerNegate fc t) (VIntegerNegate fc' t') = conv env t t'

743 |   conv env (VIntegerClamp fc t) (VIntegerClamp fc' t') = conv env t t'

744 |   conv env (VIntegerToDouble fc t) (VIntegerToDouble fc' t') = conv env t t'

745 |   conv env (VDouble fc) (VDouble fc') = pure ()

746 |   conv env (VDoubleLit fc t) (VDoubleLit fc' t') = convEq fc t t' -- TODO use binary encode

747 |   conv env (VDoubleShow fc t) (VDoubleShow fc' t') = conv env t t'

748 |   conv env (VText fc) (VText fc') = pure ()

749 |   conv env (VTextLit fc t@(MkVChunks xys z)) (VTextLit fc' u@(MkVChunks xys' z')) =

750 |     let l = strFromChunks xys

751 |         r = strFromChunks xys' in

752 |     case (l, r) of

753 |          ((Just l'), (Just r')) => do

754 |            convEq fc (l' ++ z) (r' ++ z')

755 |          _ => convChunks fc env t u

756 |   conv env (VTextAppend fc t u) (VTextAppend fc' t' u') = do

757 |     conv env t t'

758 |     conv env u u'

759 |   conv env (VTextShow fc t) (VTextShow fc' t') = do

760 |     conv env t t'

761 |   conv env (VTextReplace fc t u v) (VTextReplace fc' t' u' v') = do

762 |     conv env t t'

763 |     conv env u u'

764 |     conv env v v'

765 |   conv env (VList fc a) (VList fc' a') = conv env a a'

766 |   conv env (VListLit fc _ xs) (VListLit fc' _ xs') = convList fc env xs xs'

767 |   conv env (VListAppend fc t u) (VListAppend fc' t' u') = do

768 |     conv env t t'

769 |     conv env u u'

770 |   conv env (VListBuild fc _ t) (VListBuild fc' _ t') = conv env t t'

771 |   conv env (VListFold fc a l _ t u) (VListFold fc' a' l' _ t' u') = do

772 |     conv env a a'

773 |     conv env l l'

774 |     conv env t t'

775 |     conv env u u'

776 |   conv env (VListLength fc _ t) (VListLength fc' _ t') = conv env t t'

777 |   conv env (VListHead fc _ t) (VListHead fc' _ t') = conv env t t'

778 |   conv env (VListLast fc _ t) (VListLast fc' _ t') = conv env t t'

779 |   conv env (VListIndexed fc _ t) (VListIndexed fc' _ t') = conv env t t'

780 |   conv env (VListReverse fc _ t) (VListReverse fc' _ t') = conv env t t'

781 |   conv env (VOptional fc a) (VOptional fc' a') = conv env a a'

782 |   conv env (VNone fc _) (VNone fc' _) = pure ()