0 | module Core.TT.Term

  2 | import Algebra

  4 | import Core.FC

  6 | import Core.Name.Scoped

  7 | import Core.TT.Binder

  8 | import Core.TT.Primitive

  9 | import Core.TT.Var

 11 | import Data.List

 13 | import Libraries.Data.List.SizeOf

 15 | %default total

 22 | public export

 23 | data NameType : Type where

 24 |      Bound   : NameType

 25 |      Func    : NameType

 26 |      DataCon : (tag : Int) -> (arity : Nat) -> NameType

 27 |      TyCon   : (arity : Nat) -> NameType

 29 | %name NameType nt

 33 | Show NameType where

 34 |   showPrec d Bound = "Bound"

 35 |   showPrec d Func = "Func"

 36 |   showPrec d (DataCon tag ar) = showCon d "DataCon" $ showArg tag ++ showArg ar

 37 |   showPrec d (TyCon ar) = showCon d "TyCon" $ showArg ar

 40 | isCon : NameType -> Maybe Nat

 41 | isCon (DataCon t a) = Just a

 42 | isCon (TyCon a) = Just a

 43 | isCon _ = Nothing

 48 | public export

 49 | data LazyReason = LInf | LLazy | LUnknown

 51 | %name LazyReason lz

 55 | public export

 56 | data UseSide = UseLeft | UseRight

 58 | %name UseSide side

 60 | public export

 61 | data WhyErased a

 62 |   = Placeholder

 63 |   | Impossible

 64 |   | Dotted a

 67 | Show a => Show (WhyErased a) where

 68 |   show Placeholder = "placeholder"

 69 |   show Impossible = "impossible"

 70 |   show (Dotted x) = "dotted \{show x}"

 72 | %name WhyErased why

 75 | Functor WhyErased where

 76 |   map f Placeholder = Placeholder

 77 |   map f Impossible = Impossible

 78 |   map f (Dotted x) = Dotted (f x)

 81 | Foldable WhyErased where

 82 |   foldr c n (Dotted x) = c x n

 83 |   foldr c n _ = n

 86 | Traversable WhyErased where

 87 |   traverse f Placeholder = pure Placeholder

 88 |   traverse f Impossible = pure Impossible

 89 |   traverse f (Dotted x) = Dotted <$> f x

 95 | public export

 96 | data Term : Scoped where

 97 |      Local : FC -> (isLet : Maybe Bool) ->

 98 |              (idx : Nat) -> (0 p : IsVar name idx vars) -> Term vars

 99 |      Ref : FC -> NameType -> (name : Name) -> Term vars

100 |      -- Metavariables and the scope they are applied to

101 |      Meta : FC -> Name -> Int -> List (Term vars) -> Term vars

102 |      Bind : FC -> (x : Name) ->

103 |             (b : Binder (Term vars)) ->

104 |             (scope : Term (Scope.bind vars x)) -> Term vars

105 |      App : FC -> (fn : Term vars) -> (arg : Term vars) -> Term vars

106 |      -- as patterns; since we check LHS patterns as terms before turning

107 |      -- them into patterns, this helps us get it right. When normalising,

108 |      -- we just reduce the inner term and ignore the 'as' part

109 |      -- The 'as' part should really be a Name rather than a Term, but it's

110 |      -- easier this way since it gives us the ability to work with unresolved

111 |      -- names (Ref) and resolved names (Local) without having to define a

112 |      -- special purpose thing. (But it'd be nice to tidy that up, nevertheless)

113 |      As : FC -> UseSide -> (as : Term vars) -> (pat : Term vars) -> Term vars

114 |      -- Typed laziness annotations

115 |      TDelayed : FC -> LazyReason -> Term vars -> Term vars

116 |      TDelay : FC -> LazyReason -> (ty : Term vars) -> (arg : Term vars) -> Term vars

117 |      TForce : FC -> LazyReason -> Term vars -> Term vars

118 |      PrimVal : FC -> (c : Constant) -> Term vars

119 |      Erased : FC -> WhyErased (Term vars) -> Term vars

120 |      TType : FC -> Name -> -- universe variable

121 |              Term vars

123 | %name Term t, u

125 | public export

126 | ClosedTerm : Type

127 | ClosedTerm = Term []

132 | export covering

133 | insertNames : GenWeakenable Term

134 | insertNames out ns (Local fc r idx prf)

135 |    = let MkNVar prf' = insertNVarNames out ns (MkNVar prf) in

136 |      Local fc r _ prf'

137 | insertNames out ns (Ref fc nt name) = Ref fc nt name

138 | insertNames out ns (Meta fc name idx args)

139 |     = Meta fc name idx (map (insertNames out ns) args)

140 | insertNames out ns (Bind fc x b scope)

141 |     = Bind fc x (assert_total (map (insertNames out ns) b))

142 |            (insertNames (suc out) ns scope)

143 | insertNames out ns (App fc fn arg)

144 |     = App fc (insertNames out ns fn) (insertNames out ns arg)

145 | insertNames out ns (As fc s as tm)

146 |     = As fc s (insertNames out ns as) (insertNames out ns tm)

147 | insertNames out ns (TDelayed fc r ty) = TDelayed fc r (insertNames out ns ty)

148 | insertNames out ns (TDelay fc r ty tm)

149 |     = TDelay fc r (insertNames out ns ty) (insertNames out ns tm)

150 | insertNames out ns (TForce fc r tm) = TForce fc r (insertNames out ns tm)

151 | insertNames out ns (PrimVal fc c) = PrimVal fc c

152 | insertNames out ns (Erased fc Impossible) = Erased fc Impossible

153 | insertNames out ns (Erased fc Placeholder) = Erased fc Placeholder

154 | insertNames out ns (Erased fc (Dotted t)) = Erased fc (Dotted (insertNames out ns t))

155 | insertNames out ns (TType fc u) = TType fc u

158 | compatTerm : CompatibleVars xs ys -> Term xs -> Term ys

159 | compatTerm compat tm = believe_me tm -- no names in term, so it's identity

184 |   export

185 |   shrinkPi : Shrinkable (PiInfo . Term)

186 |   shrinkPi pinfo th

187 |     = assert_total

188 |     $ traverse (\ t => shrinkTerm t th) pinfo

190 |   export

191 |   shrinkBinder : Shrinkable (Binder . Term)

192 |   shrinkBinder binder th

193 |     = assert_total

194 |     $ traverse (\ t => shrinkTerm t th) binder

196 |   export

197 |   shrinkTerms : Shrinkable (List . Term)

198 |   shrinkTerms ts th

199 |     = assert_total

200 |     $ traverse (\ t => shrinkTerm t th) ts

202 |   shrinkTerm : Shrinkable Term

203 |   shrinkTerm (Local fc r idx loc) prf

204 |     = do MkVar loc' <- shrinkIsVar loc prf

205 |          pure (Local fc r _ loc')

206 |   shrinkTerm (Ref fc x name) prf = Just (Ref fc x name)

207 |   shrinkTerm (Meta fc x y xs) prf

208 |      = do Just (Meta fc x y !(shrinkTerms xs prf))

209 |   shrinkTerm (Bind fc x b scope) prf

210 |      = Just (Bind fc x !(shrinkBinder b prf) !(shrinkTerm scope (Keep prf)))

211 |   shrinkTerm (App fc fn arg) prf

212 |      = Just (App fc !(shrinkTerm fn prf) !(shrinkTerm arg prf))

213 |   shrinkTerm (As fc s as tm) prf

214 |      = Just (As fc s !(shrinkTerm as prf) !(shrinkTerm tm prf))

215 |   shrinkTerm (TDelayed fc x y) prf

216 |      = Just (TDelayed fc x !(shrinkTerm y prf))

217 |   shrinkTerm (TDelay fc x t y) prf

218 |      = Just (TDelay fc x !(shrinkTerm t prf) !(shrinkTerm y prf))

219 |   shrinkTerm (TForce fc r x) prf

220 |      = Just (TForce fc r !(shrinkTerm x prf))

221 |   shrinkTerm (PrimVal fc c) prf = Just (PrimVal fc c)

222 |   shrinkTerm (Erased fc Placeholder) prf = Just (Erased fc Placeholder)

223 |   shrinkTerm (Erased fc Impossible) prf = Just (Erased fc Impossible)

224 |   shrinkTerm (Erased fc (Dotted t)) prf = Erased fc . Dotted <$> shrinkTerm t prf

225 |   shrinkTerm (TType fc u) prf = Just (TType fc u)

229 |   export

230 |   thinPi : Thinnable (PiInfo . Term)

231 |   thinPi pinfo th = assert_total $ map (\ t => thinTerm t th) pinfo

233 |   export

234 |   thinBinder : Thinnable (Binder . Term)

235 |   thinBinder binder th = assert_total $ map (\ t => thinTerm t th) binder

237 |   export

238 |   thinTerms : Thinnable (List . Term)

239 |   thinTerms ts th = assert_total $ map (\ t => thinTerm t th) ts

241 |   thinTerm : Thinnable Term

242 |   thinTerm (Local fc x idx y) th

243 |       = let MkVar y' = thinIsVar y th in Local fc x _ y'

244 |   thinTerm (Ref fc x name) th = Ref fc x name

245 |   thinTerm (Meta fc x y xs) th

246 |       = Meta fc x y (thinTerms xs th)

247 |   thinTerm (Bind fc x b scope) th

248 |       = Bind fc x (thinBinder b th) (thinTerm scope (Keep th))

249 |   thinTerm (App fc fn arg) th

250 |       = App fc (thinTerm fn th) (thinTerm arg th)

251 |   thinTerm (As fc s nm pat) th

252 |       = As fc s (thinTerm nm th) (thinTerm pat th)

253 |   thinTerm (TDelayed fc x y) th = TDelayed fc x (thinTerm y th)

254 |   thinTerm (TDelay fc x t y) th

255 |       = TDelay fc x (thinTerm t th) (thinTerm y th)

256 |   thinTerm (TForce fc r x) th = TForce fc r (thinTerm x th)

257 |   thinTerm (PrimVal fc c) th = PrimVal fc c

258 |   thinTerm (Erased fc Impossible) th = Erased fc Impossible

259 |   thinTerm (Erased fc Placeholder) th = Erased fc Placeholder

260 |   thinTerm (Erased fc (Dotted t)) th = Erased fc (Dotted (thinTerm t th))

261 |   thinTerm (TType fc u) th = TType fc u

264 | GenWeaken Term where

265 |   genWeakenNs = assert_total $ insertNames

269 | WeakenTerm : Weaken Term

270 | WeakenTerm = GenWeakenWeakens

273 | FreelyEmbeddable Term where

276 | IsScoped Term where

277 |   shrink = shrinkTerm

278 |   thin = thinTerm

279 |   compatNs = compatTerm

285 | apply : FC -> Term vars -> List (Term vars) -> Term vars

286 | apply loc fn [] = fn

287 | apply loc fn (a :: args) = apply loc (App loc fn a) args

291 | applySpineWithFC : Term vars -> SnocList (FC, Term vars) -> Term vars

292 | applySpineWithFC fn [<] = fn

293 | applySpineWithFC fn (args :< (fc, arg)) = App fc (applySpineWithFC fn args) arg

297 | applyStackWithFC : Term vars -> List (FC, Term vars) -> Term vars

298 | applyStackWithFC fn [] = fn

299 | applyStackWithFC fn ((fc, arg) :: args) = applyStackWithFC (App fc fn arg) args

303 | fnType : FC -> Term vars -> Term vars -> Term vars

304 | fnType fc arg scope = Bind emptyFC (MN "_" 0) (Pi fc top Explicit arg) (weaken scope)

307 | linFnType : FC -> Term vars -> Term vars -> Term vars

308 | linFnType fc arg scope = Bind emptyFC (MN "_" 0) (Pi fc linear Explicit arg) (weaken scope)

311 | getFnArgs : Term vars -> (Term vars, List (Term vars))

312 | getFnArgs tm = getFA [] tm

313 |   where

314 |     getFA : List (Term vars) -> Term vars ->

315 |             (Term vars, List (Term vars))

316 |     getFA args (App _ f a) = getFA (a :: args) f

317 |     getFA args tm = (tm, args)

320 | getFn : Term vars -> Term vars

321 | getFn (App _ f a) = getFn f

322 | getFn tm = tm

325 | getArgs : Term vars -> (List (Term vars))

326 | getArgs = snd . getFnArgs

335 | public export

336 | interface StripNamespace a where

337 |   trimNS : Namespace -> a -> a

338 |   restoreNS : Namespace -> a -> a

341 | StripNamespace Name where

342 |   trimNS ns nm@(NS tns n)

343 |     = if ns == tns then NS emptyNS n else nm

344 |       -- ^ A blank namespace, rather than a UN, so we don't catch primitive

345 |       -- names which are represented as UN.

346 |   trimNS ns nm = nm

348 |   restoreNS ns nm@(NS tns n)

349 |       = if isNil (unsafeUnfoldNamespace tns)

350 |             then NS ns n

351 |             else nm

352 |   restoreNS ns nm = nm

354 | export covering

355 | StripNamespace (Term vars) where

356 |   trimNS ns (Ref fc x nm)

357 |       = Ref fc x (trimNS ns nm)

358 |   trimNS ns (Meta fc x y xs)

359 |       = Meta fc x y (map (trimNS ns) xs)

360 |   trimNS ns (Bind fc x b scope)

361 |       = Bind fc x (map (trimNS ns) b) (trimNS ns scope)

362 |   trimNS ns (App fc fn arg)

363 |       = App fc (trimNS ns fn) (trimNS ns arg)

364 |   trimNS ns (As fc s p tm)

365 |       = As fc s (trimNS ns p) (trimNS ns tm)

366 |   trimNS ns (TDelayed fc x y)

367 |       = TDelayed fc x (trimNS ns y)

368 |   trimNS ns (TDelay fc x t y)

369 |       = TDelay fc x (trimNS ns t) (trimNS ns y)

370 |   trimNS ns (TForce fc r y)

371 |       = TForce fc r (trimNS ns y)

372 |   trimNS ns tm = tm

374 |   restoreNS ns (Ref fc x nm)

375 |       = Ref fc x (restoreNS ns nm)

376 |   restoreNS ns (Meta fc x y xs)

377 |       = Meta fc x y (map (restoreNS ns) xs)

378 |   restoreNS ns (Bind fc x b scope)

379 |       = Bind fc x (map (restoreNS ns) b) (restoreNS ns scope)

380 |   restoreNS ns (App fc fn arg)

381 |       = App fc (restoreNS ns fn) (restoreNS ns arg)

382 |   restoreNS ns (As fc s p tm)

383 |       = As fc s (restoreNS ns p) (restoreNS ns tm)

384 |   restoreNS ns (TDelayed fc x y)

385 |       = TDelayed fc x (restoreNS ns y)

386 |   restoreNS ns (TDelay fc x t y)

387 |       = TDelay fc x (restoreNS ns t) (restoreNS ns y)

388 |   restoreNS ns (TForce fc r y)

389 |       = TForce fc r (restoreNS ns y)

390 |   restoreNS ns tm = tm

394 | isErased : Term vars -> Bool

395 | isErased (Erased {}) = True

396 | isErased _ = False

399 | getLoc : Term vars -> FC

400 | getLoc (Local fc _ _ _) = fc

401 | getLoc (Ref fc _ _) = fc

402 | getLoc (Meta fc _ _ _) = fc

403 | getLoc (Bind fc _ _ _) = fc

404 | getLoc (App fc _ _) = fc

405 | getLoc (As fc _ _ _) = fc

406 | getLoc (TDelayed fc _ _) = fc

407 | getLoc (TDelay fc _ _ _) = fc

408 | getLoc (TForce fc _ _) = fc

409 | getLoc (PrimVal fc _) = fc

410 | getLoc (Erased fc i) = fc

411 | getLoc (TType fc _) = fc

414 | Eq LazyReason where

415 |   (==) LInf LInf = True

416 |   (==) LLazy LLazy = True

417 |   (==) LUnknown LUnknown = True

418 |   (==) _ _ = False

421 | Show LazyReason where

422 |     show LInf = "Inf"

423 |     show LLazy = "Lazy"

424 |     show LUnknown = "Unkown"

427 | compatible : LazyReason -> LazyReason -> Bool

428 | compatible LUnknown _ = True

429 | compatible _ LUnknown = True

430 | compatible x y = x == y

434 | Eq a => Eq (WhyErased a) where

435 |   Placeholder == Placeholder = True

436 |   Impossible == Impossible = True

437 |   Dotted t == Dotted u = t == u

438 |   _ == _ = False

441 | eqWhyErasedBy : (a -> b -> Bool) -> WhyErased a -> WhyErased b -> Bool

442 | eqWhyErasedBy eq Impossible Impossible = True

443 | eqWhyErasedBy eq Placeholder Placeholder = True

444 | eqWhyErasedBy eq (Dotted t) (Dotted u) = eq t u

445 | eqWhyErasedBy eq _ _ = False

449 | eqTerm : Term vs -> Term vs' -> Bool

450 | eqTerm (Local _ _ idx _) (Local _ _ idx' _) = idx == idx'

451 | eqTerm (Ref _ _ n) (Ref _ _ n') = n == n'

452 | eqTerm (Meta _ _ i args) (Meta _ _ i' args')

453 |     = i == i' && assert_total (all (uncurry eqTerm) (zip args args'))

454 | eqTerm (Bind _ _ b sc) (Bind _ _ b' sc')

455 |     = assert_total (eqBinderBy eqTerm b b') && eqTerm sc sc'

456 | eqTerm (App _ f a) (App _ f' a') = eqTerm f f' && eqTerm a a'

457 | eqTerm (As _ _ a p) (As _ _ a' p') = eqTerm a a' && eqTerm p p'

458 | eqTerm (TDelayed _ _ t) (TDelayed _ _ t') = eqTerm t t'

459 | eqTerm (TDelay _ _ t x) (TDelay _ _ t' x') = eqTerm t t' && eqTerm x x'

460 | eqTerm (TForce _ _ t) (TForce _ _ t') = eqTerm t t'

461 | eqTerm (PrimVal _ c) (PrimVal _ c') = c == c'

462 | eqTerm (Erased _ i) (Erased _ i') = assert_total (eqWhyErasedBy eqTerm i i')

463 | eqTerm (TType {}) (TType {}) = True

464 | eqTerm _ _ = False

468 | Eq (Term vars) where

469 |   (==) = eqTerm

476 |   resolveNamesBinder : (vars : Scope) -> Binder (Term vars) -> Binder (Term vars)

477 |   resolveNamesBinder vars b = assert_total $ map (resolveNames vars) b

479 |   resolveNamesTerms : (vars : Scope) -> List (Term vars) -> List (Term vars)

480 |   resolveNamesTerms vars ts = assert_total $ map (resolveNames vars) ts

482 |   -- Replace any Ref Bound in a type with appropriate local

483 |   export

484 |   resolveNames : (vars : Scope) -> Term vars -> Term vars

485 |   resolveNames vars (Ref fc Bound name)

486 |       = case isNVar name vars of

487 |              Just (MkNVar prf) => Local fc (Just False) _ prf

488 |              _ => Ref fc Bound name

489 |   resolveNames vars (Meta fc n i xs)

490 |       = Meta fc n i (resolveNamesTerms vars xs)

491 |   resolveNames vars (Bind fc x b scope)

492 |       = Bind fc x (resolveNamesBinder vars b) (resolveNames (x :: vars) scope)

493 |   resolveNames vars (App fc fn arg)

494 |       = App fc (resolveNames vars fn) (resolveNames vars arg)

495 |   resolveNames vars (As fc s as pat)

496 |       = As fc s (resolveNames vars as) (resolveNames vars pat)

497 |   resolveNames vars (TDelayed fc x y)

498 |       = TDelayed fc x (resolveNames vars y)

499 |   resolveNames vars (TDelay fc x t y)

500 |       = TDelay fc x (resolveNames vars t) (resolveNames vars y)

501 |   resolveNames vars (TForce fc r x)

502 |       = TForce fc r (resolveNames vars x)

503 |   resolveNames vars tm = tm

509 | withPiInfo : Show t => PiInfo t -> String -> String

510 | withPiInfo Explicit tm = "(" ++ tm ++ ")"

511 | withPiInfo Implicit tm = "{" ++ tm ++ "}"

512 | withPiInfo AutoImplicit tm = "{auto " ++ tm ++ "}"

513 | withPiInfo (DefImplicit t) tm = "{default " ++ show t ++ " " ++ tm ++ "}"

517 | {vars : _} -> Show (Term vars) where

518 |   show tm = let (fn, args) = getFnArgs tm in showApp fn args

519 |     where

520 |       showApp : {vars : _} -> Term vars -> List (Term vars) -> String

521 |       showApp (Local _ c idx p) []

522 |          = show (nameAt p) ++ "[" ++ show idx ++ "]"

524 |       showApp (Ref _ _ n) [] = show n

525 |       showApp (Meta _ n _ args) []

526 |           = "?" ++ show n ++ "_" ++ show args

527 |       showApp (Bind _ x (Lam _ c info ty) sc) []

528 |           = "\\" ++ withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++

529 |             " => " ++ show sc

530 |       showApp (Bind _ x (Let _ c val ty) sc) []

531 |           = "let " ++ showCount c ++ show x ++ " : " ++ show ty ++

532 |             " = " ++ show val ++ " in " ++ show sc

533 |       showApp (Bind _ x (Pi _ c info ty) sc) []

534 |           = withPiInfo info (showCount c ++ show x ++ " : " ++ show ty) ++

535 |             " -> " ++ show sc

536 |       showApp (Bind _ x (PVar _ c info ty) sc) []

537 |           = withPiInfo info ("pat " ++ showCount c ++ show x ++ " : " ++ show ty) ++

538 |             " => " ++ show sc

539 |       showApp (Bind _ x (PLet _ c val ty) sc) []

540 |           = "plet " ++ showCount c ++ show x ++ " : " ++ show ty ++

541 |             " = " ++ show val ++ " in " ++ show sc

542 |       showApp (Bind _ x (PVTy _ c ty) sc) []

543 |           = "pty " ++ showCount c ++ show x ++ " : " ++ show ty ++

544 |             " => " ++ show sc

545 |       showApp (App {}) [] = "[can't happen]"

546 |       showApp (As _ _ n tm) [] = show n ++ "@" ++ show tm

547 |       showApp (TDelayed _ _ tm) [] = "%Delayed " ++ show tm

548 |       showApp (TDelay _ _ _ tm) [] = "%Delay " ++ show tm

549 |       showApp (TForce _ _ tm) [] = "%Force " ++ show tm

550 |       showApp (PrimVal _ c) [] = show c

551 |       showApp (Erased _ (Dotted t)) [] = ".(" ++ show t ++ ")"

552 |       showApp (Erased {}) [] = "[__]"

553 |       showApp (TType _ u) [] = "Type"

554 |       showApp _ [] = "???"

555 |       showApp f args = "(" ++ assert_total (show f) ++ " " ++

556 |                         assert_total (showSep " " (map show args))

557 |                      ++ ")"