Built with doc-gen4, running Lean4. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+โ†‘Ctrl+โ†“to navigate, Ctrl+๐Ÿ–ฑ๏ธto focus. On Mac, use Cmdinstead of Ctrl. 
/-
Copyright (c) 2022 Gabriel Ebner. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Gabriel Ebner, Mario Carneiro
-/
import Lean.PrettyPrinter.Delaborator.Builtins
import Std.Lean.Delaborator
open Lean Meta Std

namespace Std.Tactic.Coe

/-- The different types of coercions that are supported by the `coe` attribute. -/
inductive 
CoeFnType: Type
CoeFnType
  /-- The basic coercion `โ†‘x`, see `CoeT.coe` -/
  | 
coe: CoeFnType
coe
  /-- The coercion to a function type, see `CoeFun.coe` -/
  | 
coeFun: CoeFnType
coeFun
  /-- The coercion to a type, see `CoeSort.coe` -/
  | 
coeSort: CoeFnType
coeSort
  deriving 
Inhabited: Sort u โ†’ Sort (max1u)
Inhabited, 
Repr: Type u โ†’ Type u
Repr, 
DecidableEq: Sort u โ†’ Sort (max1u)
DecidableEq


instance: ToExpr CoeFnType
instance : 
ToExpr: Type ?u.1005 โ†’ Type ?u.1005
ToExpr 
CoeFnType: Type
CoeFnType where
  toTypeExpr := 
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
CoeFnType: Type
CoeFnType
  toExpr := open CoeFnType in fun
    | 
coe: CoeFnType
coe => 
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
coe: CoeFnType
coe
    | 
coeFun: CoeFnType
coeFun => 
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
coeFun: CoeFnType
coeFun
    | 
coeSort: CoeFnType
coeSort => 
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
coeSort: CoeFnType
coeSort

/-- Information associated to a coercion function to enable sensible delaboration. -/
structure 
CoeFnInfo: Type
CoeFnInfo where
  /-- The number of arguments to the coercion function -/
  
numArgs: CoeFnInfo โ†’ Nat
numArgs : 
Nat: Type
Nat
  /-- The argument index that represents the value being coerced -/
  
coercee: CoeFnInfo โ†’ Nat
coercee : 
Nat: Type
Nat
  /-- The type of coercion -/
  
type: CoeFnInfo โ†’ CoeFnType
type : 
CoeFnType: Type
CoeFnType
  deriving 
Inhabited: Sort u โ†’ Sort (max1u)
Inhabited, 
Repr: Type u โ†’ Type u
Repr


instance: ToExpr CoeFnInfo
instance : 
ToExpr: Type ?u.3441 โ†’ Type ?u.3441
ToExpr 
CoeFnInfo: Type
CoeFnInfo where
  toTypeExpr := 
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
CoeFnInfo: Type
CoeFnInfo
  toExpr | โŸจ
a: Nat
a, 
b: Nat
b, 
c: CoeFnType
cโŸฉ => 
mkApp3: Expr โ†’ Expr โ†’ Expr โ†’ Expr โ†’ Expr
mkApp3 (
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
CoeFnInfo.mk: Nat โ†’ Nat โ†’ CoeFnType โ†’ CoeFnInfo
CoeFnInfo.mk) (
toExpr: {ฮฑ : Type ?u.3471} โ†’ [self : ToExpr ฮฑ] โ†’ ฮฑ โ†’ Expr
toExpr 
a: Nat
a) (
toExpr: {ฮฑ : Type ?u.3484} โ†’ [self : ToExpr ฮฑ] โ†’ ฮฑ โ†’ Expr
toExpr 
b: Nat
b) (
toExpr: {ฮฑ : Type ?u.3496} โ†’ [self : ToExpr ฮฑ] โ†’ ฮฑ โ†’ Expr
toExpr 
c: CoeFnType
c)

/-- The environment extension for tracking coercion functions for delaboration -/
initialize 
coeExt: SimpleScopedEnvExtension (Name ร— CoeFnInfo) (NameMap CoeFnInfo)
coeExt : 
SimpleScopedEnvExtension: Type โ†’ Type โ†’ Type
SimpleScopedEnvExtension (
Name: Type
Name ร— 
CoeFnInfo: Type
CoeFnInfo) (
NameMap: Type โ†’ Type
NameMap 
CoeFnInfo: Type
CoeFnInfo) โ†
  
registerSimpleScopedEnvExtension: {ฮฑ ฯƒ : Type} โ†’ SimpleScopedEnvExtension.Descr ฮฑ ฯƒ โ†’ IO (SimpleScopedEnvExtension ฮฑ ฯƒ)
registerSimpleScopedEnvExtension {
    addEntry := fun 
st: ?m.3771
st (
n: Name
n, 
i: CoeFnInfo
i) => 
st: ?m.3771
st.
insert: {ฮฑ : Type} โ†’ NameMap ฮฑ โ†’ Name โ†’ ฮฑ โ†’ RBMap Name ฮฑ Name.quickCmp
insert 
n: Name
n 
i: CoeFnInfo
i
    initial := 
{}: ?m.3871
{}
  }

/-- Lookup the coercion information for a given function -/
def 
getCoeFnInfo?: Name โ†’ CoreM (Option CoeFnInfo)
getCoeFnInfo? (
fn: Name
fn : 
Name: Type
Name) : 
CoreM: Type โ†’ Type
CoreM (
Option: Type ?u.4245 โ†’ Type ?u.4245
Option 
CoeFnInfo: Type
CoeFnInfo) :=
  return (
coeExt: SimpleScopedEnvExtension (Name ร— CoeFnInfo) (NameMap CoeFnInfo)
coeExt.
getState: {ฯƒ ฮฑ ฮฒ : Type} โ†’ [inst : Inhabited ฯƒ] โ†’ ScopedEnvExtension ฮฑ ฮฒ ฯƒ โ†’ Environment โ†’ ฯƒ
getState 
(โ† getEnv): ?m.4314
(โ† 
getEnv: {m : Type โ†’ Type} โ†’ [self : MonadEnv m] โ†’ m Environment
getEnv
(โ† getEnv): ?m.4314
)).
find?: {ฮฑ : Type} โ†’ NameMap ฮฑ โ†’ Name โ†’ Option ฮฑ
find? 
fn: Name
fn

open PrettyPrinter.Delaborator SubExpr

/--
This delaborator tries to elide functions which are known coercions.
For example, `Int.ofNat` is a coercion, so instead of printing `ofNat n` we just print `โ†‘n`,
and when re-parsing this we can (usually) recover the specific coercion being used.
-/
def 
coeDelaborator: CoeFnInfo โ†’ Delab
coeDelaborator (
info: CoeFnInfo
info : 
CoeFnInfo: Type
CoeFnInfo) : 
Delab: Type
Delab := 
whenPPOption: (Options โ†’ Bool) โ†’ Delab โ†’ Delab
whenPPOption 
getPPCoercions: Options โ†’ Bool
getPPCoercions do
  
withOverApp: Nat โ†’ Delab โ†’ Delab
withOverApp 
info: CoeFnInfo
info.
numArgs: CoeFnInfo โ†’ Nat
numArgs do
    
`(โ†‘$(โ† withNaryArg info.coercee delab)): ?m.5744 ?m.5747
`(โ†‘$(โ† 
withNaryArg: {ฮฑ : Type} โ†’
  {m : Type โ†’ Type} โ†’
    [inst : Monad m] โ†’ [inst : MonadReaderOf SubExpr m] โ†’ [inst : MonadWithReaderOf SubExpr m] โ†’ Nat โ†’ m ฮฑ โ†’ m ฮฑ
withNaryArg
`(โ†‘$(โ† withNaryArg info.coercee delab)): ?m.5744 ?m.5747
 
info: CoeFnInfo
info
`(โ†‘$(โ† withNaryArg info.coercee delab)): ?m.5744 ?m.5747
.
coercee: CoeFnInfo โ†’ Nat
coercee
`(โ†‘$(โ† withNaryArg info.coercee delab)): ?m.5744 ?m.5747
 
delab: Delab
delab
`(โ†‘$(โ† withNaryArg info.coercee delab)): ?m.5744 ?m.5747
))

/-- Add a coercion delaborator for the given function. -/
def 
addCoeDelaborator: Name โ†’ CoeFnInfo โ†’ MetaM Unit
addCoeDelaborator (
name: Name
name : 
Name: Type
Name) (
info: CoeFnInfo
info : 
CoeFnInfo: Type
CoeFnInfo) : 
MetaM: Type โ†’ Type
MetaM 
Unit: Type
Unit := do
  let 
delabName: ?m.9165
delabName := 
name: Name
name ++ 
`delaborator: Name
`delaborator
  
addAndCompile: Declaration โ†’ CoreM Unit
addAndCompile <| 
Declaration.defnDecl: DefinitionVal โ†’ Declaration
Declaration.defnDecl {
    name := 
delabName: ?m.9165
delabName
    levelParams := 
[]: List ?m.9246
[]
    type := 
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
Delab: Type
Delab
    value := 
mkApp: Expr โ†’ Expr โ†’ Expr
mkApp (
mkConst: Name โ†’ optParam (List Level) [] โ†’ Expr
mkConst ``
coeDelaborator: CoeFnInfo โ†’ Delab
coeDelaborator) (
toExpr: {ฮฑ : Type ?u.9248} โ†’ [self : ToExpr ฮฑ] โ†’ ฮฑ โ†’ Expr
toExpr 
info: CoeFnInfo
info)
    hints := 
.opaque: ReducibilityHints
.opaque
    safety := 
.safe: DefinitionSafety
.safe
  }
  let 
kind: ?m.9372
kind := 
`app: Name
`app ++ 
name: Name
name
  
Attribute.add: Name โ†’ Name โ†’ Syntax โ†’ optParam AttributeKind AttributeKind.global โ†’ AttrM Unit
Attribute.add 
delabName: ?m.9165
delabName 
`delab: Name
`delab (
Unhygienic.run: {ฮฑ : Type} โ†’ Unhygienic ฮฑ โ†’ ฮฑ
Unhygienic.run `(
attr: Parser.Category
attr| delab $(
mkIdent: Name โ†’ Ident
mkIdent 
kind: ?m.9372
kind):ident))

/-- Add `name` to the coercion extension and add a coercion delaborator for the function. -/
def 
registerCoercion: Name โ†’ optParam (Option CoeFnInfo) none โ†’ MetaM Unit
registerCoercion (
name: Name
name : 
Name: Type
Name) (
info: optParam (Option CoeFnInfo) none
info : 
Option: Type ?u.12225 โ†’ Type ?u.12225
Option 
CoeFnInfo: Type
CoeFnInfo := 
none: {ฮฑ : Type ?u.12226} โ†’ Option ฮฑ
none) : 
MetaM: Type โ†’ Type
MetaM 
Unit: Type
Unit := do
  let 
info: ?m.12265
info โ† match 
info: optParam (Option CoeFnInfo) none
info with | 
some: {ฮฑ : Type ?u.12273} โ†’ ฮฑ โ†’ Option ฮฑ
some 
info: CoeFnInfo
info => 
pure: {f : Type ?u.12324 โ†’ Type ?u.12323} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.12324} โ†’ ฮฑ โ†’ f ฮฑ
pure
pure info: MetaM (?m.12269 yโœ)
 
info: CoeFnInfo
info | 
none: {ฮฑ : Type ?u.12413} โ†’ Option ฮฑ
none => do
    let 
fnInfo: ?m.12732
fnInfo โ† 
getFunInfo: Expr โ†’ MetaM FunInfo
getFunInfo 
(โ† mkConstWithLevelParams name): ?m.12683
(โ† 
mkConstWithLevelParams: {m : Type โ†’ Type} โ†’ [inst : Monad m] โ†’ [inst : MonadEnv m] โ†’ [inst : MonadError m] โ†’ Name โ†’ m Expr
mkConstWithLevelParams
(โ† mkConstWithLevelParams name): ?m.12683
 
name: Name
name
(โ† mkConstWithLevelParams name): ?m.12683
)
    let 
some: {ฮฑ : Type ?u.12749} โ†’ ฮฑ โ†’ Option ฮฑ
some 
coercee: Nat
coercee := 
fnInfo: ?m.12732
fnInfo.
paramInfo: FunInfo โ†’ Array ParamInfo
paramInfo.
findIdx?: {ฮฑ : Type ?u.12736} โ†’ Array ฮฑ โ†’ (ฮฑ โ†’ Bool) โ†’ Option Nat
findIdx? (ยท.
binderInfo: ParamInfo โ†’ BinderInfo
binderInfo.
isExplicit: BinderInfo โ†’ Bool
isExplicit)
      | 
throwError "{name} has no explicit arguments": MetaM (?m.12269 yโœ)
throwError
throwError "{name} has no explicit arguments": MetaM (?m.12269 yโœ)
 "{
name: Name
name
throwError "{name} has no explicit arguments": MetaM (?m.12269 yโœ)
} has no explicit arguments"
    
pure: {f : Type ?u.12800 โ†’ Type ?u.12799} โ†’ [self : Pure f] โ†’ {ฮฑ : Type ?u.12800} โ†’ ฮฑ โ†’ f ฮฑ
pure
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
 { numArgs
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
 := 
coercee: Nat
coercee
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
 + 
1: ?m.12964
1
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
, coercee
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
, type
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
 := 
.coe: CoeFnType
.coe
pure { numArgs := coercee + 1, coercee, type := .coe }: MetaM (?m.12269 yโœ)
 }
  
modifyEnv: {m : Type โ†’ Type} โ†’ [self : MonadEnv m] โ†’ (Environment โ†’ Environment) โ†’ m Unit
modifyEnv (
coeExt: SimpleScopedEnvExtension (Name ร— CoeFnInfo) (NameMap CoeFnInfo)
coeExt.
addEntry: {ฮฑ ฮฒ ฯƒ : Type} โ†’ ScopedEnvExtension ฮฑ ฮฒ ฯƒ โ†’ Environment โ†’ ฮฒ โ†’ Environment
addEntry ยท (
name: Name
name, 
info: ?m.12265
info))
  
addCoeDelaborator: Name โ†’ CoeFnInfo โ†’ MetaM Unit
addCoeDelaborator 
name: Name
name 
info: ?m.12265
info

/--
The `@[coe]` attribute on a function (which should also appear in a
`instance : Coe A B := โŸจmyFnโŸฉ` declaration) allows the delaborator to show
applications of this function as `โ†‘` when printing expressions.
-/
syntax (name := Attr.coe) "coe" : 
attr: Parser.Category
attr

initialize 
registerBuiltinAttribute: AttributeImpl โ†’ IO Unit
registerBuiltinAttribute {
  name := 
`coe: Name
`coe
  descr := 
"Adds a definition as a coercion": String
"Adds a definition as a coercion"
  add := fun 
decl: ?m.15158
decl 
_stx: ?m.15161
_stx 
kind: ?m.15164
kind => 
MetaM.run': {ฮฑ : Type} โ†’
  MetaM ฮฑ โ†’
    optParam Meta.Context
        {
          config :=
            { foApprox := false, ctxApprox := false, quasiPatternApprox := false, constApprox := false,
              isDefEqStuckEx := false, transparency := TransparencyMode.default, zetaNonDep := true, trackZeta := false,
              unificationHints := true, proofIrrelevance := true, assignSyntheticOpaque := false, offsetCnstrs := true,
              etaStruct := EtaStructMode.all },
          lctx :=
            {
              fvarIdToDecl :=
                { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
              decls :=
                { root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
                  tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
                  shift := PersistentArray.initShift, tailOff := 0 } },
          localInstances := #[], defEqCtx? := none, synthPendingDepth := 0, canUnfold? := none } โ†’
      optParam Meta.State
          {
            mctx :=
              { depth := 0, levelAssignDepth := 0, mvarCounter := 0,
                lDepth := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                decls := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                userNames :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                lAssignment :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                eAssignment :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                dAssignment :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
            cache :=
              {
                inferType :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                funInfo := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                synthInstance :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                whnfDefault :=
                  { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                whnfAll := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 },
                defEq := { root := PersistentHashMap.Node.entries PersistentHashMap.mkEmptyEntriesArray, size := 0 } },
            zetaFVarIds := โˆ…,
            postponed :=
              { root := PersistentArrayNode.node (Array.mkEmpty (USize.toNat PersistentArray.branching)),
                tail := Array.mkEmpty (USize.toNat PersistentArray.branching), size := 0,
                shift := PersistentArray.initShift, tailOff := 0 } } โ†’
        CoreM ฮฑ
MetaM.run' do
    unless 
kind: ?m.15164
kind == 
.global: AttributeKind
.global do
      
throwError "cannot add local or scoped coe attribute": ?m.15454 ?m.15455
throwError
throwError "cannot add local or scoped coe attribute": ?m.15454 ?m.15455
 "cannot add local or scoped coe attribute"
    
registerCoercion: Name โ†’ optParam (Option CoeFnInfo) none โ†’ MetaM Unit
registerCoercion 
decl: ?m.15158
decl
}