0 | module Core.TT

  2 | import public Core.FC

  3 | import public Core.Name

  4 | import public Core.Name.Scoped

  6 | import Data.Maybe

  8 | import Libraries.Data.NameMap

  9 | import Libraries.Text.PrettyPrint.Prettyprinter

 10 | import Libraries.Text.PrettyPrint.Prettyprinter.Util

 12 | import Libraries.Data.List.SizeOf

 13 | import Libraries.Data.SnocList.SizeOf

 15 | import public Algebra

 17 | import public Core.TT.Binder

 18 | import public Core.TT.Primitive

 19 | import public Core.TT.Subst

 20 | import public Core.TT.Term

 21 | import public Core.TT.Term.Subst

 22 | import public Core.TT.Var

 24 | %default covering

 26 | public export

 27 | record KindedName where

 28 |   constructor MkKindedName

 29 |   nameKind : Maybe NameType

 30 |   fullName : Name -- fully qualified name

 31 |   rawName  : Name

 33 | %name KindedName kn

 36 | defaultKindedName : Name -> KindedName

 37 | defaultKindedName nm = MkKindedName Nothing nm nm

 40 | funKindedName : Name -> KindedName

 41 | funKindedName nm = MkKindedName (Just Func) nm nm

 44 | Show KindedName where show = show . rawName

 48 | [Raw] Show KindedName where

 49 |   showPrec d (MkKindedName nm fn rn) =

 50 |     showCon d "MkKindedName" $ showArg nm ++ showArg @{Raw} fn ++ showArg @{Raw} rn

 52 | namespace CList

 53 |   -- A list correspoding to another list

 54 |   public export

 55 |   data CList : List a -> Type -> Type where

 56 |        Nil : CList [] ty

 57 |        (::) : (x : ty) -> CList cs ty -> CList (c :: cs) ty

 60 | public export

 61 | data Visibility = Private | Export | Public

 62 | %name Visibility vis

 65 | Show Visibility where

 66 |   show Private = "private"

 67 |   show Export = "export"

 68 |   show Public = "public export"

 71 | Pretty Void Visibility where

 72 |   pretty Private = pretty "private"

 73 |   pretty Export = pretty "export"

 74 |   pretty Public = pretty "public" <++> pretty "export"

 77 | Eq Visibility where

 78 |   Private == Private = True

 79 |   Export == Export = True

 80 |   Public == Public = True

 81 |   _ == _ = False

 84 | Ord Visibility where

 85 |   compare Private Export = LT

 86 |   compare Private Public = LT

 87 |   compare Export Public = LT

 89 |   compare Private Private = EQ

 90 |   compare Export Export = EQ

 91 |   compare Public Public = EQ

 93 |   compare Export Private = GT

 94 |   compare Public Private = GT

 95 |   compare Public Export = GT

 97 | public export

 98 | data DataOpt : Type where

 99 |      SearchBy : List1 Name -> DataOpt -- determining arguments

100 |      NoHints : DataOpt -- Don't generate search hints for constructors

101 |      UniqueSearch : DataOpt -- auto implicit search must check result is unique

102 |      External : DataOpt -- implemented externally

103 |      NoNewtype : DataOpt -- don't apply newtype optimisation

104 | %name DataOpt dopt

107 | Eq DataOpt where

108 |   (==) (SearchBy xs) (SearchBy ys) = xs == ys

109 |   (==) NoHints NoHints = True

110 |   (==) UniqueSearch UniqueSearch = True

111 |   (==) External External = True

112 |   (==) NoNewtype NoNewtype = True

113 |   (==) _ _ = False

115 | public export

116 | data Fixity = InfixL | InfixR | Infix | Prefix

119 | Show Fixity where

120 |   show InfixL = "infixl"

121 |   show InfixR = "infixr"

122 |   show Infix  = "infix"

123 |   show Prefix = "prefix"

126 | Interpolation Fixity where

127 |   interpolate = show

130 | Eq Fixity where

131 |   InfixL == InfixL = True

132 |   InfixR == InfixR = True

133 |   Infix == Infix = True

134 |   Prefix == Prefix = True

135 |   _ == _ = False

138 | public export

139 | data BindingModifier = NotBinding | Autobind | Typebind

142 | Eq BindingModifier where

143 |   NotBinding == NotBinding = True

144 |   Autobind == Autobind = True

145 |   Typebind == Typebind = True

146 |   _ == _ = False

149 | Show BindingModifier where

150 |   show NotBinding = "regular"

151 |   show Typebind = "typebind"

152 |   show Autobind = "autobind"

155 | Interpolation BindingModifier where

156 |   interpolate = show

159 | public export

160 | record FixityInfo where

161 |   constructor MkFixityInfo

162 |   fc : FC

163 |   vis : Visibility

164 |   bindingInfo : BindingModifier

165 |   fix : Fixity

166 |   precedence : Nat

169 | Show FixityInfo where

170 |   show fx = "fc: \{show fx.fc}, visibility: \{show fx.vis}, binding: \{show fx.bindingInfo}, fixity: \{show fx.fix}, precedence: \{show fx.precedence}"

174 | Eq FixityInfo where

175 |   x == y = x.fc == y.fc

176 |         && x.vis == y.vis

177 |         && x.bindingInfo == y.bindingInfo

178 |         && x.fix == y.fix

179 |         && x.precedence == y.precedence

186 | public export

187 | data FixityDeclarationInfo = UndeclaredFixity | DeclaredFixity FixityInfo

197 | public export

198 | data OperatorLHSInfo : tm -> Type where

199 |   -- Traditional operator wihtout binding, carries the lhs

200 |   NoBinder : (lhs : tm) -> OperatorLHSInfo tm

201 |   -- (nm : ty) =@ fn x

202 |   BindType : (name : tm) -> (ty : tm) -> OperatorLHSInfo tm

203 |   -- (nm := exp) =@ fn nm

204 |   BindExpr : (name : tm) -> (expr : tm) -> OperatorLHSInfo tm

205 |   -- (nm : ty := exp) =@ fn nm

206 |   BindExplicitType : (name : tm) ->  (type, expr : tm) -> OperatorLHSInfo tm

209 | Show (OperatorLHSInfo tm) where

210 |   show (NoBinder lhs)                    = "regular"

211 |   show (BindType name ty)                = "type-binding (typebind)"

212 |   show (BindExpr name expr)              = "automatically-binding (autobind)"

213 |   show (BindExplicitType name type expr) = "automatically-binding (autobind)"

215 | %name OperatorLHSInfo opInfo

218 | Functor OperatorLHSInfo where

219 |   map f (NoBinder lhs) = NoBinder $ f lhs

220 |   map f (BindType nm lhs) = BindType (f nm) (f lhs)

221 |   map f (BindExpr nm lhs) = BindExpr (f nm) (f lhs)

222 |   map f (BindExplicitType nm ty lhs) = BindExplicitType (f nm) (f ty) (f lhs)

225 | (.getLhs) : OperatorLHSInfo tm -> tm

226 | (.getLhs) (NoBinder lhs) = lhs

227 | (.getLhs) (BindExpr _ lhs) = lhs

228 | (.getLhs) (BindType _ lhs) = lhs

229 | (.getLhs) (BindExplicitType _ _ lhs) = lhs

232 | (.getBoundPat) : OperatorLHSInfo tm -> Maybe tm

233 | (.getBoundPat) (NoBinder lhs) = Nothing

234 | (.getBoundPat) (BindType name ty) = Just name

235 | (.getBoundPat) (BindExpr name expr) = Just name

236 | (.getBoundPat) (BindExplicitType name type expr) = Just name

239 | (.getBinder) : OperatorLHSInfo tm -> BindingModifier

240 | (.getBinder) (NoBinder lhs) = NotBinding

241 | (.getBinder) (BindType name ty) = Typebind

242 | (.getBinder) (BindExpr name expr) = Autobind

243 | (.getBinder) (BindExplicitType name type expr) = Autobind

245 | public export

246 | data TotalReq = Total | CoveringOnly | PartialOK

247 | %name TotalReq treq

250 | Eq TotalReq where

251 |     (==) Total Total = True

252 |     (==) CoveringOnly CoveringOnly = True

253 |     (==) PartialOK PartialOK = True

254 |     (==) _ _ = False

259 | Ord TotalReq where

260 |   PartialOK <= _ = True

261 |   _ <= Total = True

262 |   a <= b = a == b

264 |   a < b = a <= b && a /= b

267 | Show TotalReq where

268 |     show Total = "total"

269 |     show CoveringOnly = "covering"

270 |     show PartialOK = "partial"

273 | public export

274 | data PartialReason

275 |        = NotStrictlyPositive

276 |        | BadCall (List Name)

277 |        -- sequence of mutually-recursive function calls leading to a non-terminating function

278 |        | BadPath (List (FC, Name)) Name

279 |        | RecPath (List (FC, Name))

282 | Show PartialReason where

283 |   show NotStrictlyPositive = "not strictly positive"

284 |   show (BadCall [n])

285 |       = "possibly not terminating due to call to " ++ show n

286 |   show (BadCall ns)

287 |       = "possibly not terminating due to calls to " ++ showSep ", " (map show ns)

288 |   show (BadPath [_] n)

289 |       = "possibly not terminating due to call to " ++ show n

290 |   show (BadPath init n)

291 |       = "possibly not terminating due to function " ++ show n ++ " being reachable via " ++ showSep " -> " (map show init)

292 |   show (RecPath loop)

293 |       = "possibly not terminating due to recursive path " ++ showSep " -> " (map (show . snd) loop)

296 | Pretty Void PartialReason where

297 |   pretty NotStrictlyPositive = reflow "not strictly positive"

298 |   pretty (BadCall [n])

299 |     = reflow "possibly not terminating due to call to" <++> pretty n

300 |   pretty (BadCall ns)

301 |     = reflow "possibly not terminating due to calls to" <++> concatWith (surround (comma <+> space)) (pretty <$> ns)

302 |   pretty (BadPath [_] n)

303 |     = reflow "possibly not terminating due to call to" <++> pretty n

304 |   pretty (BadPath init n)

305 |     = reflow "possibly not terminating due to function" <++> pretty n

306 |       <++> reflow "being reachable via"

307 |       <++> concatWith (surround (pretty " -> ")) (pretty <$> map snd init)

308 |   pretty (RecPath loop)

309 |     = reflow "possibly not terminating due to recursive path" <++> concatWith (surround (pretty " -> ")) (pretty <$> map snd loop)

311 | public export

312 | data Terminating

313 |        = Unchecked

314 |        | IsTerminating

315 |        | NotTerminating PartialReason

318 | Show Terminating where

319 |   show Unchecked = "not yet checked"

320 |   show IsTerminating = "terminating"

321 |   show (NotTerminating p) = show p

324 | Pretty Void Terminating where

325 |   pretty Unchecked = reflow "not yet checked"

326 |   pretty IsTerminating = pretty "terminating"

327 |   pretty (NotTerminating p) = pretty p

329 | public export

330 | data Covering

331 |        = IsCovering

332 |        | MissingCases (List ClosedTerm)

333 |        | NonCoveringCall (List Name)

336 | Show Covering where

337 |   show IsCovering = "covering"

338 |   show (MissingCases c) = "not covering all cases"

339 |   show (NonCoveringCall [f])

340 |      = "not covering due to call to function " ++ show f

341 |   show (NonCoveringCall cs)

342 |      = "not covering due to calls to functions " ++ showSep ", " (map show cs)

345 | Pretty Void Covering where

346 |   pretty IsCovering = pretty "covering"

347 |   pretty (MissingCases c) = reflow "not covering all cases"

348 |   pretty (NonCoveringCall [f])

349 |      = reflow "not covering due to call to function" <++> pretty f

350 |   pretty (NonCoveringCall cs)

351 |      = reflow "not covering due to calls to functions" <++> concatWith (surround (comma <+> space)) (pretty <$> cs)

355 | public export

356 | record Totality where

357 |      constructor MkTotality

358 |      isTerminating : Terminating

359 |      isCovering : Covering

362 | Show Totality where

363 |   show tot

364 |     = let t = isTerminating tot

365 |           c = isCovering tot in

366 |         showTot t c

367 |     where

368 |       showTot : Terminating -> Covering -> String

369 |       showTot IsTerminating IsCovering = "total"

370 |       showTot IsTerminating c = show c

371 |       showTot t IsCovering = show t

372 |       showTot t c = show c ++ "; " ++ show t

375 | Pretty Void Totality where

376 |   pretty (MkTotality IsTerminating IsCovering) = pretty "total"

377 |   pretty (MkTotality IsTerminating c) = pretty c

378 |   pretty (MkTotality t IsCovering) = pretty t

379 |   pretty (MkTotality t c) = pretty c <+> semi <++> pretty t

382 | unchecked : Totality

383 | unchecked = MkTotality Unchecked IsCovering

386 | isTotal : Totality

387 | isTotal = MkTotality Unchecked IsCovering

390 | notCovering : Totality

391 | notCovering = MkTotality Unchecked (MissingCases [])

393 | namespace Bounds

394 |   public export

395 |   data Bounds : Scoped where

396 |        None : Bounds Scope.empty

397 |        Add : (x : Name) -> Name -> Bounds xs -> Bounds (x :: xs)

398 |        -- TODO add diagonal constructor

400 |   export

401 |   sizeOf : Bounds xs -> SizeOf xs

402 |   sizeOf None        = zero

403 |   sizeOf (Add _ _ b) = suc (sizeOf b)

406 | addVars : SizeOf outer -> Bounds bound ->

407 |           NVar name (outer ++ vars) ->

408 |           NVar name (outer ++ (bound ++ vars))

409 | addVars p = insertNVarNames p . sizeOf

412 | resolveRef : SizeOf outer ->

413 |              SizeOf done ->

414 |              Bounds bound -> FC -> Name ->

415 |              Maybe (Var (outer ++ (done <>> bound ++ vars)))

416 | resolveRef _ _ None _ _ = Nothing

417 | resolveRef {outer} {vars} {done} p q (Add {xs} new old bs) fc n

418 |     = if n == old

419 |          then Just (weakenNs p (mkVarChiply q))

420 |          else resolveRef p (q :< new) bs fc n

422 | mkLocals : SizeOf outer -> Bounds bound ->

423 |            Term (outer ++ vars) -> Term (outer ++ (bound ++ vars))

424 | mkLocals outer bs (Local fc r idx p)

425 |     = let MkNVar p' = addVars outer bs (MkNVar p) in Local fc r _ p'

426 | mkLocals outer bs (Ref fc Bound name)

427 |     = fromMaybe (Ref fc Bound name) $ do

428 |         MkVar p <- resolveRef outer [<] bs fc name

429 |         pure (Local fc Nothing _ p)

430 | mkLocals outer bs (Ref fc nt name)

431 |     = Ref fc nt name

432 | mkLocals outer bs (Meta fc name y xs)

433 |     = fromMaybe (Meta fc name y (map (mkLocals outer bs) xs)) $ do

434 |         MkVar p <- resolveRef outer [<] bs fc name

435 |         pure (Local fc Nothing _ p)

436 | mkLocals outer bs (Bind fc x b scope)

437 |     = Bind fc x (map (mkLocals outer bs) b)

438 |            (mkLocals (suc outer) bs scope)

439 | mkLocals outer bs (App fc fn arg)

440 |     = App fc (mkLocals outer bs fn) (mkLocals outer bs arg)

441 | mkLocals outer bs (As fc s as tm)

442 |     = As fc s (mkLocals outer bs as) (mkLocals outer bs tm)

443 | mkLocals outer bs (TDelayed fc x y)

444 |     = TDelayed fc x (mkLocals outer bs y)

445 | mkLocals outer bs (TDelay fc x t y)

446 |     = TDelay fc x (mkLocals outer bs t) (mkLocals outer bs y)

447 | mkLocals outer bs (TForce fc r x)

448 |     = TForce fc r (mkLocals outer bs x)

449 | mkLocals outer bs (PrimVal fc c) = PrimVal fc c

450 | mkLocals outer bs (Erased fc Impossible) = Erased fc Impossible

451 | mkLocals outer bs (Erased fc Placeholder) = Erased fc Placeholder

452 | mkLocals outer bs (Erased fc (Dotted t)) = Erased fc (Dotted (mkLocals outer bs t))

453 | mkLocals outer bs (TType fc u) = TType fc u

456 | refsToLocals : Bounds bound -> Term vars -> Term (bound ++ vars)

457 | refsToLocals None y = y

458 | refsToLocals bs y = mkLocals zero  bs y

462 | refToLocal : (x : Name) -> (new : Name) -> Term vars -> Term (new :: vars)

463 | refToLocal x new tm = refsToLocals (Add new x None) tm

467 | substName : Name -> Term vars -> Term vars -> Term vars

468 | substName x new (Ref fc nt name)

469 |     = case nameEq x name of

470 |            Nothing => Ref fc nt name

471 |            Just Refl => new

472 | substName x new (Meta fc n i xs)

473 |     = Meta fc n i (map (substName x new) xs)

476 | substName x new (Bind fc y b scope)

477 |     = Bind fc y (map (substName x new) b) (substName x (weaken new) scope)

478 | substName x new (App fc fn arg)

479 |     = App fc (substName x new fn) (substName x new arg)

480 | substName x new (As fc s as pat)

481 |     = As fc s as (substName x new pat)

482 | substName x new (TDelayed fc y z)

483 |     = TDelayed fc y (substName x new z)

484 | substName x new (TDelay fc y t z)

485 |     = TDelay fc y (substName x new t) (substName x new z)

486 | substName x new (TForce fc r y)

487 |     = TForce fc r (substName x new y)

488 | substName x new tm = tm

491 | addMetas : (usingResolved : Bool) -> NameMap Bool -> Term vars -> NameMap Bool

492 | addMetas res ns (Local fc x idx y) = ns

493 | addMetas res ns (Ref fc x name) = ns

494 | addMetas res ns (Meta fc n i xs)

495 |   = addMetaArgs (insert (ifThenElse res (Resolved i) n) False ns) xs

496 |   where

497 |     addMetaArgs : NameMap Bool -> List (Term vars) -> NameMap Bool

498 |     addMetaArgs ns [] = ns

499 |     addMetaArgs ns (t :: ts) = addMetaArgs (addMetas res ns t) ts

500 | addMetas res ns (Bind fc x (Let _ c val ty) scope)

501 |     = addMetas res (addMetas res (addMetas res ns val) ty) scope

502 | addMetas res ns (Bind fc x b scope)

503 |     = addMetas res (addMetas res ns (binderType b)) scope

504 | addMetas res ns (App fc fn arg)

505 |     = addMetas res (addMetas res ns fn) arg

506 | addMetas res ns (As fc s as tm) = addMetas res ns tm

507 | addMetas res ns (TDelayed fc x y) = addMetas res ns y

508 | addMetas res ns (TDelay fc x t y)

509 |     = addMetas res (addMetas res ns t) y

510 | addMetas res ns (TForce fc r x) = addMetas res ns x

511 | addMetas res ns (PrimVal fc c) = ns

512 | addMetas res ns (Erased fc i) = foldr (flip $ addMetas res) ns i

513 | addMetas res ns (TType fc u) = ns

517 | getMetas : Term vars -> NameMap Bool

518 | getMetas tm = addMetas False empty tm

521 | addRefs : (underAssert : Bool) -> (aTotal : Name) ->

522 |           NameMap Bool -> Term vars -> NameMap Bool

523 | addRefs ua at ns (Local fc x idx y) = ns

524 | addRefs ua at ns (Ref fc x name) = insert name ua ns

525 | addRefs ua at ns (Meta fc n i xs)

526 |     = addRefsArgs ns xs

527 |   where

528 |     addRefsArgs : NameMap Bool -> List (Term vars) -> NameMap Bool

529 |     addRefsArgs ns [] = ns

530 |     addRefsArgs ns (t :: ts) = addRefsArgs (addRefs ua at ns t) ts

531 | addRefs ua at ns (Bind fc x (Let _ c val ty) scope)

532 |     = addRefs ua at (addRefs ua at (addRefs ua at ns val) ty) scope

533 | addRefs ua at ns (Bind fc x b scope)

534 |     = addRefs ua at (addRefs ua at ns (binderType b)) scope

535 | addRefs ua at ns (App _ (App _ (Ref fc _ name) x) y)

536 |     = if name == at

537 |          then addRefs True at (insert name True ns) y

538 |          else addRefs ua at (addRefs ua at (insert name ua ns) x) y

539 | addRefs ua at ns (App fc fn arg)

540 |     = addRefs ua at (addRefs ua at ns fn) arg

541 | addRefs ua at ns (As fc s as tm) = addRefs ua at ns tm

542 | addRefs ua at ns (TDelayed fc x y) = addRefs ua at ns y

543 | addRefs ua at ns (TDelay fc x t y)

544 |     = addRefs ua at (addRefs ua at ns t) y

545 | addRefs ua at ns (TForce fc r x) = addRefs ua at ns x

546 | addRefs ua at ns (PrimVal fc c) = ns

547 | addRefs ua at ns (Erased fc i) = foldr (flip $ addRefs ua at) ns i

548 | addRefs ua at ns (TType fc u) = ns

554 | getRefs : (aTotal : Name) -> Term vars -> NameMap Bool

555 | getRefs at tm = addRefs False at empty tm