From beec014890cc9f25df3d07d65c5eefcb5d332ee4 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Mon, 25 Mar 2019 16:10:49 +0100 Subject: [PATCH] =?UTF-8?q?feat(library/init/lean/{parser/term,expander}):?= =?UTF-8?q?=20remove=20`(x=20:=20e)=20=E2=86=92=20f`=20macro=20hack=20and?= =?UTF-8?q?=20replace=20with=20actual=20parser?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- library/init/lean/expander.lean | 60 ++++++++++-------------------- library/init/lean/parser/term.lean | 8 ++++ 2 files changed, 27 insertions(+), 41 deletions(-) diff --git a/library/init/lean/expander.lean b/library/init/lean/expander.lean index c3c87a5571..a377bf2e8c 100644 --- a/library/init/lean/expander.lean +++ b/library/init/lean/expander.lean @@ -64,9 +64,15 @@ instance coeIdentIdentUnivs : HasCoe SyntaxIdent identUnivs.View := instance coeIdentBinderId : HasCoe SyntaxIdent binderIdent.View := ⟨binderIdent.View.id⟩ -instance coeBindersExt {α : Type} [HasCoeT α binderIdent.View] : HasCoe (List α) Term.bindersExt.View := +instance coeIdentsBindersExt {α : Type} [HasCoeT α binderIdent.View] : HasCoe (List α) Term.bindersExt.View := ⟨λ ids, {leadingIds := ids.map coe}⟩ +instance coeBracketedBinderMixedBinder : HasCoe bracketedBinder.View mixedBinder.View := +⟨mixedBinder.View.bracketed⟩ + +instance coeMixedBindersBindersExt {α : Type} [HasCoeT α mixedBinder.View] : HasCoe (List α) Term.bindersExt.View := +⟨λ mbs, {leadingIds := [], remainder := some $ bindersRemainder.View.mixed $ mbs.map coe}⟩ + instance coeBindersExtBinders : HasCoe Term.bindersExt.View Term.binders.View := ⟨Term.binders.View.extended⟩ @@ -311,43 +317,20 @@ def pi.transform : transformer := let v := view pi stx, expandBinders (λ binders body, review pi {op := v.op, binders := binders, range := body}) v.binders v.range -def getAppArgs : Syntax → (Syntax × List Syntax) -| stx := match tryView app stx with - | some v := let (fn, args) := getAppArgs v.fn in (fn, v.Arg::args) - | none := (stx, []) - -def termToIdentsUnivs : Syntax → List identUnivs.View × Option Syntax -| stx := match stx.kind with - | some @identUnivs := ([view identUnivs stx], none) - | some @app := - let v := view app stx in - (match tryView identUnivs v.fn with - | some id := - let (ids, rem) := termToIdentsUnivs v.Arg in (id::ids, rem) - | none := ([], some stx)) - | _ := ([], some stx) - -def termToExplicitBinder (stx : Syntax) : Option explicitBinder.View := do - v ← tryView paren stx, - {Term := t, special := parenSpecial.View.typed pst} ← v.content | failure, - (ids, none) ← pure $ termToIdentsUnivs t | failure, - let bids := ids.map $ λ id, binderIdent.View.id id.id, - pure {content := explicitBinderContent.View.other {ids := bids, type := some $ {type := pst.type}}} +def depArrow.transform : transformer := +λ stx, do + let v := view depArrow stx, + pure $ review pi { + op := Syntax.atom {val := "Π"}, + binders := binders.View.extended [v.binder], + range := v.range} def arrow.transform : transformer := λ stx, do let v := view arrow stx, - -- if `stx` is of the form `(id... : e)... → f`, use the type expressions as binders - -- Ex: `(a : b) -> c` ~> `Π (a : b), c` - let (fn, args) := getAppArgs v.dom, - let groups := fn::args, pure $ review pi { op := Syntax.atom {val := "Π"}, - binders := match groups.mmap termToExplicitBinder with - | some bnders := binders.View.extended { - leadingIds := [], - remainder := bindersRemainder.View.mixed $ bnders.map (mixedBinder.View.bracketed ∘ bracketedBinder.View.explicit)} - | none := binders.View.simple $ simpleBinder.View.explicit {id := `a, type := v.dom}, + binders := binders.View.simple $ simpleBinder.View.explicit {id := `a, type := v.dom}, range := v.range} def paren.transform : transformer := @@ -388,9 +371,7 @@ def let.transform : transformer := | letLhs.View.id lli@{id := _, binders := [], type := none} := pure $ review «let» {v with lhs := letLhs.View.id {lli with type := some {type := review hole {}}}} | letLhs.View.id lli@{id := _, binders := _, type := ty} := - let bindrs := binders.View.extended { - leadingIds := [], - remainder := bindersRemainder.View.mixed $ lli.binders.map mixedBinder.View.bracketed} in + let bindrs := binders.View.extended lli.binders in pure $ review «let» {v with lhs := letLhs.View.id { id := lli.id, @@ -408,9 +389,7 @@ def axiom.transform : transformer := let v := view «axiom» stx, match v with | {sig := {params := bracketedBinders.View.extended bindrs, type := type}, ..} := do - let bindrs := binders.View.extended { - leadingIds := [], - remainder := bindersRemainder.View.mixed $ bindrs.map mixedBinder.View.bracketed}, + let bindrs := binders.View.extended bindrs, pure $ review «axiom» {v with sig := { params := bracketedBinders.View.simple [], type := {type := review pi {op := Syntax.atom {val := "Π"}, binders := bindrs, range := type.type}}}} @@ -441,9 +420,7 @@ def introRule.transform : transformer := let v := view «introRule» stx, match v.sig with | {params := bracketedBinders.View.extended bindrs, type := some type} := do - let bindrs := binders.View.extended { - leadingIds := [], - remainder := bindersRemainder.View.mixed $ bindrs.map mixedBinder.View.bracketed}, + let bindrs := binders.View.extended bindrs, pure $ review «introRule» {v with sig := { params := bracketedBinders.View.simple [], type := some {type := review pi {op := Syntax.atom {val := "Π"}, binders := bindrs, @@ -508,6 +485,7 @@ def builtinTransformers : RBMap Name transformer (<) := RBMap.fromList [ (bracketedBinders.name, bracketedBinders.transform), (lambda.name, lambda.transform), (pi.name, pi.transform), + (depArrow.name, depArrow.transform), (arrow.name, arrow.transform), (paren.name, paren.transform), (assume.name, assume.transform), diff --git a/library/init/lean/parser/term.lean b/library/init/lean/parser/term.lean index 0967226099..d436ccb426 100644 --- a/library/init/lean/parser/term.lean +++ b/library/init/lean/parser/term.lean @@ -345,6 +345,11 @@ def borrowPrec := maxPrec - 1 def borrowed.Parser : termParser := node! borrowed ["@&":maxPrec, Term: Term.Parser borrowPrec] +--- Agda's `(x : e) → f` +@[derive Parser.HasTokens Parser.HasView] +def depArrow.Parser : termParser := +node! depArrow [binder: bracketedBinder.Parser, op: unicodeSymbol "→" "->" 25, range: Term.Parser 24] + -- TODO(Sebastian): replace with attribute @[derive HasTokens] def builtinLeadingParsers : TokenMap termParser := TokenMap.ofList [ @@ -352,6 +357,7 @@ def builtinLeadingParsers : TokenMap termParser := TokenMap.ofList [ (number.name, number.Parser), (stringLit.name, stringLit.Parser), ("(", paren.Parser), + ("(", depArrow.Parser), ("_", hole.Parser), ("Sort", sort.Parser), ("Type", sort.Parser), @@ -372,6 +378,8 @@ def builtinLeadingParsers : TokenMap termParser := TokenMap.ofList [ ("if", if.Parser), ("{", structInst.Parser), ("{", Subtype.Parser), + ("{", depArrow.Parser), + ("[", depArrow.Parser), (".(", inaccessible.Parser), ("._", anonymousInaccessible.Parser), ("sorry", sorry.Parser),