Lean.Elab.Extra

Lean.Elab.Term.elabForIn.getMonad expectedType? = match expectedType? with | none => Lean.throwError (Lean.toMessageData "invalid 'for_in%' notation, expected type is not available") | some expectedType => do let a ← Lean.Elab.Term.isTypeApp? expectedType match a with | some (m, x) => pure m | none => Lean.throwError (Lean.toMessageData "invalid 'for_in%' notation, expected type is not of of the form `M α`" ++ Lean.toMessageData (Lean.indentExpr expectedType) ++ Lean.toMessageData "")

source

def Lean.Elab.Term.elabForIn.throwFailure (forInInstance : Lean.Expr) :

Lean.Elab.TermElabM Lean.Expr

Equations

Lean.Elab.Term.elabForIn.throwFailure forInInstance = Lean.throwError (Lean.toMessageData "failed to synthesize instance for 'for_in%' notation" ++ Lean.toMessageData (Lean.indentExpr forInInstance) ++ Lean.toMessageData "")

source

def Lean.Elab.Term.BinOp.elabBinOp :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.BinOp.elabBinOp stx expectedType? = do let tree ← Lean.Elab.Term.BinOp.toTree stx let r ← Lean.Elab.Term.BinOp.analyze tree expectedType? let cls : Lean.Name := `Elab.binop let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Expr := fun y => if (r.hasUncomparable || Option.isNone r.max?) = true then do let result ← Lean.Elab.Term.BinOp.toExpr tree Lean.Elab.Term.ensureHasType expectedType? result none else do let a ← Lean.Elab.Term.BinOp.applyCoe tree (Option.get! r.max?) let result ← Lean.Elab.Term.BinOp.toExpr a let cls : Lean.Name := `Elab.binop let a ← Lean.isTracingEnabledFor cls let _do_jp : Unit → Lean.Elab.TermElabM Lean.Expr := fun y => Lean.Elab.Term.ensureHasType expectedType? result none if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "result: " ++ Lean.toMessageData result ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y if a = true then do let y ← Lean.addTrace cls (Lean.toMessageData "hasUncomparable: " ++ Lean.toMessageData r.hasUncomparable ++ Lean.toMessageData ", maxType: " ++ Lean.toMessageData r.max? ++ Lean.toMessageData "") _do_jp y else do let y ← pure PUnit.unit _do_jp y

source

def Lean.Elab.Term.BinOp.elabBinOpLazy :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.BinOp.elabBinOpLazy = Lean.Elab.Term.BinOp.elabBinOp

source

def Lean.Elab.Term.BinOp.elabBinCalc :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.BinOp.elabBinCalc stx expectedType? = let stepStxs := Lean.Syntax.getArgs (Lean.Syntax.getOp stx 1); let proofs := #[]; let types := #[]; do let r ← forIn stepStxs { fst := types, snd := proofs } fun stepStx r => let types := r.fst; let proofs := r.snd; do let type ← Lean.Elab.Term.elabType (Lean.Syntax.getOp stepStx 0) let discr ← liftM (Lean.Elab.Term.BinOp.relation? type) match discr with | some (x, lhs, x_1) => let _do_jp := fun types proofs y => let types := Array.push types type; do let proof ← Lean.Elab.Term.elabTermEnsuringType (Lean.Syntax.getOp stepStx 2) (some type) true true none Lean.Elab.Term.synthesizeSyntheticMVars true false let proofs : Array Lean.Expr := Array.push proofs proof pure PUnit.unit pure (ForInStep.yield { fst := types, snd := proofs }); if Array.size types > 0 then do let discr ← liftM (Lean.Elab.Term.BinOp.relation? (Array.back types)) match discr with | some (x, x_2, prevRhs) => do let a ← liftM (Lean.Meta.isDefEqGuarded lhs prevRhs) if a = true then do let y ← pure PUnit.unit _do_jp types proofs y else do let a ← liftM (Lean.Meta.inferType lhs) let a_1 ← liftM (Lean.Meta.inferType prevRhs) let y ← Lean.throwErrorAt (Lean.Syntax.getOp stepStx 0) (Lean.toMessageData "invalid 'calc' step, left-hand-side is " ++ Lean.toMessageData (Lean.indentD (Lean.toMessageData "" ++ Lean.toMessageData lhs ++ Lean.toMessageData " : " ++ Lean.toMessageData a ++ Lean.toMessageData "")) ++ Lean.toMessageData "\nprevious right-hand-side is" ++ Lean.toMessageData (Lean.indentD (Lean.toMessageData "" ++ Lean.toMessageData prevRhs ++ Lean.toMessageData " : " ++ Lean.toMessageData a_1 ++ Lean.toMessageData "")) ++ Lean.toMessageData "") _do_jp types proofs y | x => do let y ← panicWithPosWithDecl "Lean.Elab.Extra" "Lean.Elab.Term.BinOp.elabBinCalc" 290 56 "unreachable code has been reached" _do_jp types proofs y else do let y ← pure PUnit.unit _do_jp types proofs y | x => do Lean.throwErrorAt (Lean.Syntax.getOp stepStx 0) (Lean.toMessageData "invalid 'calc' step, relation expected" ++ Lean.toMessageData (Lean.indentExpr type) ++ Lean.toMessageData "") pure (ForInStep.yield { fst := types, snd := proofs }) let x : MProd (Array Lean.Expr) (Array Lean.Expr) := r match x with | { fst := types, snd := proofs } => let result := Array.getOp proofs 0; let resultType := Array.getOp types 0; do let r ← let col := { start := 1, stop := Array.size proofs, step := 1 }; forIn col { fst := resultType, snd := result } fun i r => let resultType := r.fst; let result := r.snd; do let discr ← liftM (Lean.Elab.Term.BinOp.relation? resultType) match discr with | some (r, a, b) => do let a_1 ← liftM (Lean.Meta.instantiateMVars (Array.getOp types i)) let discr ← liftM (Lean.Elab.Term.BinOp.relation? a_1) match discr with | some (s, x, c) => do let a_2 ← liftM (Lean.Meta.inferType a) let a_3 ← liftM (Lean.Meta.inferType b) let a_4 ← liftM (Lean.Meta.inferType c) let x : Lean.Expr × Lean.Expr × Lean.Expr := (a_2, a_3, a_4) match x with | (α, β, γ) => do let a_5 ← liftM (Lean.Meta.getLevel α) let a_6 ← liftM (Lean.Meta.getLevel β) let a_7 ← liftM (Lean.Meta.getLevel γ) let x : Lean.Level × Lean.Level × Lean.Level := (a_5, a_6, a_7) match x with | (u_1, u_2, u_3) => do let a_8 ← liftM (Lean.Meta.mkArrow γ (Lean.mkSort Lean.levelZero)) let a_9 ← liftM (Lean.Meta.mkArrow α a_8) let t ← liftM (Lean.Meta.mkFreshExprMVar (some a_9) Lean.MetavarKind.natural Lean.Name.anonymous) let selfType : Lean.Expr := Lean.mkAppN (Lean.mkConst `Trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t] let a_10 ← liftM (Lean.Meta.trySynthInstance selfType none) let _do_jp : Lean.Expr → Lean.Expr → PUnit → Lean.Elab.TermElabM (ForInStep (MProd Lean.Expr Lean.Expr)) := fun resultType result y => do pure () pure (ForInStep.yield { fst := resultType, snd := result }) match a_10 with | Lean.LOption.some self => let result := Lean.mkAppN (Lean.mkConst `Trans.trans [u_1, u_2, u_3]) #[α, β, γ, r, s, t, self, a, b, c, result, Array.getOp proofs i]; do let a ← liftM (Lean.Meta.inferType result) let a ← liftM (Lean.Meta.instantiateMVars a) let resultType : Lean.Expr := Lean.Expr.headBeta a let a ← liftM (Lean.Elab.Term.BinOp.relation? resultType) if Option.isSome a = true then do let y ← pure PUnit.unit _do_jp resultType result y else do let y ← Lean.throwErrorAt (Array.getOp stepStxs i) (Lean.toMessageData "invalid 'calc' step, step result is not a relation" ++ Lean.toMessageData (Lean.indentExpr resultType) ++ Lean.toMessageData "") _do_jp resultType result y | x => do let y ← Lean.throwErrorAt (Array.getOp stepStxs i) (Lean.toMessageData "invalid 'calc' step, failed to synthesize `Trans` instance" ++ Lean.toMessageData (Lean.indentExpr selfType) ++ Lean.toMessageData "") _do_jp resultType result y | x => do panicWithPosWithDecl "Lean.Elab.Extra" "Lean.Elab.Term.BinOp.elabBinCalc" 301 67 "unreachable code has been reached" pure (ForInStep.yield { fst := resultType, snd := result }) | x => do panicWithPosWithDecl "Lean.Elab.Extra" "Lean.Elab.Term.BinOp.elabBinCalc" 300 48 "unreachable code has been reached" pure (ForInStep.yield { fst := resultType, snd := result }) let x : MProd Lean.Expr Lean.Expr := r match x with | { fst := resultType, snd := result } => Lean.Elab.Term.ensureHasType expectedType? result none

source

def Lean.Elab.Term.BinOp.elabDefaultOrNonempty :

Lean.Elab.Term.TermElab

Equations

Lean.Elab.Term.BinOp.elabDefaultOrNonempty stx expectedType? = do Lean.Elab.Term.tryPostponeIfNoneOrMVar expectedType? match expectedType? with | none => Lean.throwError (Lean.toMessageData "invalid 'default_or_ofNonempty%', expected type is not known") | some expectedType => tryCatch (liftM (Lean.Meta.mkDefault expectedType)) fun ex => tryCatch (liftM (Lean.Meta.mkOfNonempty expectedType)) fun x => throw ex