max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove old notation

Browse source
This commit is contained in:
Leonardo de Moura 2021-10-02 15:03:52 -07:00
parent 74329f6713
commit acd21052c0
9 changed files with 37 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Init/Notation.lean
View file

@ -359,7 +359,7 @@ syntax (name := delta) "delta " ident (location)? : tactic
-- Auxiliary macro for lifting have/suffices/let/...
-- It makes sure the "continuation" `?_` is the main goal after refining
macro "refine_lift " e:term : tactic => `(focus (refine noImplicitLambda% $e; rotate_right))
macro "refine_lift " e:term : tactic => `(focus (refine no_implicit_lambda% $e; rotate_right))
macro "have " d:haveDecl : tactic => `(refine_lift have $d:haveDecl; ?_)
/- We use a priority > default, to avoid ambiguity with previous `have` notation -/
@ -372,7 +372,7 @@ macro_rules
| `(tactic| let rec $d:letRecDecls) => `(tactic| refine_lift let rec $d:letRecDecls; ?_)
-- Similar to `refineLift`, but using `refine'`
macro "refine_lift' " e:term : tactic => `(focus (refine' noImplicitLambda% $e; rotate_right))
macro "refine_lift' " e:term : tactic => `(focus (refine' no_implicit_lambda% $e; rotate_right))
macro "have' " d:haveDecl : tactic => `(refine_lift' have $d:haveDecl; ?_)
macro (priority := high) "have'" x:ident " := " p:term : tactic => `(have' $x:ident : _ := $p)
macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)

16
src/Lean/Elab/Do.lean
View file

@ -275,7 +275,7 @@ def mkAuxDeclFor {m} [Monad m] [MonadQuotation m] (e : Syntax) (mkCont : Syntax
let yName := y.getId
let doElem ← `(doElem| let y ← $e:term)
-- Add elaboration hint for producing sane error message
let y ← `(ensureExpectedType% "type mismatch, result value" $y)
let y ← `(ensure_expected_type% "type mismatch, result value" $y)
let k ← mkCont y
pure $ Code.decl #[yName] doElem k
@ -977,7 +977,7 @@ def reassignToTerm (reassign : Syntax) (k : Syntax) : MacroM Syntax := withRef r
-- letIdDecl := leading_parser ident >> many (ppSpace >> bracketedBinder) >> optType >> " := " >> termParser
let x := arg[0]
let val := arg[4]
let newVal ← `(ensureTypeOf% $x $(quote "invalid reassignment, value") $val)
let newVal ← `(ensure_type_of% $x $(quote "invalid reassignment, value") $val)
let arg := arg.setArg 4 newVal
let letDecl := mkNode `Lean.Parser.Term.letDecl #[arg]
`(let $letDecl:letDecl; $k)
@ -997,7 +997,7 @@ def mkIte (optIdent : Syntax) (cond : Syntax) (thenBranch : Syntax) (elseBranch
``(if $h:ident : $cond then $thenBranch else $elseBranch)
def mkJoinPoint (j : Name) (ps : Array (Name × Bool)) (body : Syntax) (k : Syntax) : M Syntax := withRef body <| withFreshMacroScope do
let pTypes ← ps.mapM fun ⟨id, useTypeOf⟩ => do if useTypeOf then `(typeOf% $(← mkIdentFromRef id)) else `(_)
let pTypes ← ps.mapM fun ⟨id, useTypeOf⟩ => do if useTypeOf then `(type_of% $(← mkIdentFromRef id)) else `(_)
let ps ← ps.mapM fun ⟨id, useTypeOf⟩ => mkIdentFromRef id
/-
We use `let_delayed` instead of `let` for joinpoints to make sure `$k` is elaborated before `$body`.
@ -1417,20 +1417,20 @@ mutual
let uvarsTuple ← liftMacroM do mkTuple (← uvars.mapM mkIdentFromRef)
if hasReturn forInBodyCodeBlock.code then
let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
let forInTerm ← `(forIn% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
let forInTerm ← `(for_in% $(xs) (MProd.mk none $uvarsTuple) fun $x r => let r := r.2; $forInBody)
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r.2;
match r.1 with
| none => Pure.pure (ensureExpectedType% "type mismatch, 'for'" PUnit.unit)
| some a => return ensureExpectedType% "type mismatch, 'for'" a)
| none => Pure.pure (ensure_expected_type% "type mismatch, 'for'" PUnit.unit)
| some a => return ensure_expected_type% "type mismatch, 'for'" a)
doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
else
let forInBody ← liftMacroM <| destructTuple uvars (← `(r)) forInBody
let forInTerm ← `(forIn% $(xs) $uvarsTuple fun $x r => $forInBody)
let forInTerm ← `(for_in% $(xs) $uvarsTuple fun $x r => $forInBody)
if doElems.isEmpty then
let auxDo ← `(do let r ← $forInTerm:term;
$uvarsTuple:term := r;
Pure.pure (ensureExpectedType% "type mismatch, 'for'" PUnit.unit))
Pure.pure (ensure_expected_type% "type mismatch, 'for'" PUnit.unit))
doSeqToCode <| getDoSeqElems (getDoSeq auxDo)
else
let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)

10
src/Lean/Elab/Extra.lean
View file

@ -45,9 +45,9 @@ open Meta
@[builtinTermElab forInMacro] def elabForIn : TermElab := fun stx expectedType? => do
match stx with
| `(forIn% $col $init $body) =>
| `(for_in% $col $init $body) =>
match (← isLocalIdent? col) with
| none => elabTerm (← `(let col := $col; forIn% col $init $body)) expectedType?
| none => elabTerm (← `(let col := $col; for_in% col $init $body)) expectedType?
| some colFVar =>
tryPostponeIfNoneOrMVar expectedType?
let m ← getMonad expectedType?
@ -69,13 +69,13 @@ open Meta
where
getMonad (expectedType? : Option Expr) : TermElabM Expr := do
match expectedType? with
| none => throwError "invalid 'forIn%' notation, expected type is not available"
| none => throwError "invalid 'for_in%' notation, expected type is not available"
| some expectedType =>
match (← isTypeApp? expectedType) with
| some (m, _) => return m
| none => throwError "invalid 'forIn%' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
| none => throwError "invalid 'for_in%' notation, expected type is not of of the form `M α`{indentExpr expectedType}"
throwFailure (forInInstance : Expr) : TermElabM Expr :=
throwError "failed to synthesize instance for 'forIn%' notation{indentExpr forInInstance}"
throwError "failed to synthesize instance for 'for_in%' notation{indentExpr forInInstance}"
namespace BinOp
/-

2
src/Lean/Elab/Term.lean
View file

@ -1121,7 +1121,7 @@ private def isTacticBlock (stx : Syntax) : Bool :=
private def isNoImplicitLambda (stx : Syntax) : Bool :=
match stx with
| `(noImplicitLambda% $x:term) => true
| `(no_implicit_lambda% $x:term) => true
| _ => false
private def isTypeAscription (stx : Syntax) : Bool :=

10
src/Lean/Parser/Term.lean
View file

@ -207,12 +207,12 @@ def matchAltsWhereDecls := leading_parser matchAlts >> optional whereDecls
@[builtinTermParser] def binop := leading_parser "binop% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def binop_lazy := leading_parser "binop_lazy% " >> ident >> ppSpace >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser ("forIn% " <|> "for_in% ") >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def forInMacro := leading_parser "for_in% " >> termParser maxPrec >> termParser maxPrec >> termParser maxPrec
@[builtinTermParser] def typeOf := leading_parser ("typeOf% " <|> "type_of% ") >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := leading_parser ("ensureTypeOf% " <|> "ensure_type_of% ") >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := leading_parser ("ensureExpectedType% " <|> "ensure_expected_type% ") >> strLit >> termParser maxPrec
@[builtinTermParser] def noImplicitLambda := leading_parser ("noImplicitLambda% " <|> "no_implicit_lambda% ") >> termParser maxPrec
@[builtinTermParser] def typeOf := leading_parser "type_of% " >> termParser maxPrec
@[builtinTermParser] def ensureTypeOf := leading_parser "ensure_type_of% " >> termParser maxPrec >> strLit >> termParser
@[builtinTermParser] def ensureExpectedType := leading_parser "ensure_expected_type% " >> strLit >> termParser maxPrec
@[builtinTermParser] def noImplicitLambda := leading_parser "no_implicit_lambda% " >> termParser maxPrec
def namedArgument := leading_parser atomic ("(" >> ident >> " := ") >> termParser >> ")"
def ellipsis := leading_parser ".."

2
src/Lean/Syntax.lean
View file

@ -228,7 +228,7 @@ def topDown (stx : Syntax) (firstChoiceOnly := false) : TopDown := ⟨firstChoic
partial instance : ForIn m TopDown Syntax where
forIn := fun ⟨firstChoiceOnly, stx⟩ init f => do
let rec @[specialize] loop stx b [Inhabited (typeOf% b)] := do
let rec @[specialize] loop stx b [Inhabited (type_of% b)] := do
match (← f stx b) with
| ForInStep.yield b' =>
let mut b := b'

6
tests/lean/run/impLambdaTac.lean
View file

@ -8,9 +8,9 @@ example (P : Prop) : ∀ {p : P}, P := by
exact @id _
example (P : Prop) : ∀ {p : P}, P := by
exact noImplicitLambda% id
exact no_implicit_lambda% id
macro "exact'" x:term : tactic => `(exact noImplicitLambda% $x)
macro "exact'" x:term : tactic => `(exact no_implicit_lambda% $x)
example (P : Prop) : ∀ {p : P}, P := by
exact' id
@ -23,7 +23,7 @@ example (P : Prop) : ∀ p : P, P := by
apply id
example (P : Prop) : ∀ {p : P}, P := by
refine noImplicitLambda% (have : _ := 1; ?_)
refine no_implicit_lambda% (have : _ := 1; ?_)
apply id
example (P : Prop) : ∀ {p : P}, P := by

18
tests/lean/typeOf.lean
View file

@ -1,29 +1,29 @@
--
def f1 (x : Nat) (b : Bool) : typeOf% x :=
let r : typeOf% (x+1) := x+1;
def f1 (x : Nat) (b : Bool) : type_of% x :=
let r : type_of% (x+1) := x+1;
r + 1
theorem ex1 : f1 1 true = 3 :=
rfl
def f2 (x : Nat) (b : Bool) : typeOf% x :=
let r : typeOf% b := x+1; -- error
def f2 (x : Nat) (b : Bool) : type_of% x :=
let r : type_of% b := x+1; -- error
r + 1
def f3 (x : Nat) (b : Bool) : typeOf% b :=
let r (x!1 : typeOf% x) : typeOf% b := x > 1;
def f3 (x : Nat) (b : Bool) : type_of% b :=
let r (x!1 : type_of% x) : type_of% b := x > 1;
r x
def f4 (x : Nat) : Nat :=
let y : Nat := x
let y := ensureTypeOf% y "invalid reassignment, term" y == 1 -- error
let y := ensure_type_of% y "invalid reassignment, term" y == 1 -- error
y + 1
def f5 (x : Nat) : Nat :=
let y : Nat := x
let y := ensureTypeOf% y "invalid reassignment, term" (y+1)
let y := ensure_type_of% y "invalid reassignment, term" (y+1)
y + 1
def f6 (x : Nat) : Nat :=
ensureExpectedType% "natural number expected, value" true
ensure_expected_type% "natural number expected, value" true

6
tests/lean/typeOf.lean.expected.out
View file

@ -1,12 +1,12 @@
typeOf.lean:11:21-11:24: error: failed to synthesize instance
typeOf.lean:11:22-11:25: error: failed to synthesize instance
HAdd Nat Nat Bool
typeOf.lean:12:0-12:5: error: failed to synthesize instance
HAdd Bool Nat Nat
typeOf.lean:20:54-20:60: error: invalid reassignment, term has type
typeOf.lean:20:56-20:62: error: invalid reassignment, term has type
Bool : Type
but is expected to have type
Nat : Type
typeOf.lean:29:53-29:57: error: natural number expected, value has type
typeOf.lean:29:55-29:59: error: natural number expected, value has type
Bool : Type
but is expected to have type
Nat : Type