From 6c16deded4700ebc62fba1ee40b217f40b45f78d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 12 Feb 2020 13:38:01 -0800 Subject: [PATCH] feat: improve implicit lambdas --- src/Init/Lean/Elab/App.lean | 31 +++++++++---------- src/Init/Lean/Elab/Binders.lean | 37 +++++++++++++++-------- tests/lean/run/newfrontend5.lean | 52 ++++++++++++++++++++++++++++++++ 3 files changed, 90 insertions(+), 30 deletions(-) create mode 100644 tests/lean/run/newfrontend5.lean diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean index 30944ce5d9..bb61f27697 100644 --- a/src/Init/Lean/Elab/App.lean +++ b/src/Init/Lean/Elab/App.lean @@ -494,17 +494,8 @@ private partial def elabAppFn (ref : Syntax) : Syntax → List LVal → Array Na -- Remark: `id.` should already have been expanded us ← if us.isEmpty then pure [] else elabExplicitUniv (us.get! 0); elabAppFnId ref id us lvals namedArgs args expectedType? explicit acc - | `(@($f:fun)) => do - s ← observing $ do { - if lvals.isEmpty && namedArgs.isEmpty && args.isEmpty then - elabFunCore f expectedType? true - else do - f ← elabFunCore f none true; - elabAppLVals ref f lvals namedArgs args expectedType? true - }; - pure $ acc.push s - | `(@$f) => - elabAppFn f lvals namedArgs args expectedType? true acc + | `(@$id:id) => + elabAppFn id lvals namedArgs args expectedType? true acc | _ => do s ← observing $ do { f ← elabTerm f none; @@ -580,7 +571,18 @@ def elabAtom : TermElab := fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType? @[builtinTermElab «id»] def elabId : TermElab := elabAtom -@[builtinTermElab explicit] def elabExplicit : TermElab := elabAtom + +@[builtinTermElab explicit] def elabExplicit : TermElab := +fun stx expectedType? => match_syntax stx with + | `(@$f:fun) => elabFunCore f expectedType? true + | `(@($f:fun)) => elabFunCore f expectedType? true + | `(@($f:fun : $type)) => do + type ← elabType type; + f ← elabFunCore f type true; + ensureHasType stx type f + | `(@$id:id) => elabAtom stx expectedType? + | _ => throwUnsupportedSyntax + @[builtinTermElab choice] def elabChoice : TermElab := elabAtom @[builtinTermElab proj] def elabProj : TermElab := elabAtom @[builtinTermElab arrayRef] def elabArrayRef : TermElab := elabAtom @@ -588,11 +590,6 @@ fun stx expectedType? => elabAppAux stx stx #[] #[] expectedType? but it is nice to have a handler for them because it allows `macros` to insert them into terms. -/ @[builtinTermElab ident] def elabRawIdent : TermElab := elabAtom -@[builtinTermElab «fun»] def elabFun : TermElab := -fun stx expectedType? => do - f ← elabFunCore stx expectedType? false; - elabAppArgs stx f #[] #[] none false - @[builtinTermElab sortApp] def elabSortApp : TermElab := fun stx _ => do u ← elabLevel (stx.getArg 1); diff --git a/src/Init/Lean/Elab/Binders.lean b/src/Init/Lean/Elab/Binders.lean index 15fd7c7c2d..0c14703ad8 100644 --- a/src/Init/Lean/Elab/Binders.lean +++ b/src/Init/Lean/Elab/Binders.lean @@ -243,7 +243,6 @@ expandFunBindersAux binders body 0 #[] namespace FunBinders structure State := -(implicitArgs : Array Expr := #[]) (fvars : Array Expr := #[]) (lctx : LocalContext) (localInsts : LocalInstances) @@ -267,20 +266,29 @@ private partial def elabFunBinderViews (binderViews : Array BinderView) : Nat if h : i < binderViews.size then let binderView := binderViews.get ⟨i, h⟩; withLCtx s.lctx s.localInsts $ do + let s := if binderView.bi.isExplicit then { explicit := true, .. s } else s; type ← elabType binderView.type; - fvarId ← mkFreshFVarId; + fvarId ← mkFreshFVarId; let fvar := mkFVar fvarId; - let fvars := s.fvars.push fvar; - -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type); - let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi; - s ← propagateExpectedType binderView.id fvar type s; - className? ← isClass binderView.type type; - match className? with - | none => elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, .. s } - | some className => do - resetSynthInstanceCache; - let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId }; - elabFunBinderViews (i+1) { fvars := fvars, lctx := lctx, localInsts := localInsts, .. s } + let s := { fvars := s.fvars.push fvar, .. s }; + let continue (s : State) : TermElabM State := do { + className? ← isClass binderView.type type; + match className? with + | none => elabFunBinderViews (i+1) s + | some className => do + resetSynthInstanceCache; + let localInsts := s.localInsts.push { className := className, fvar := mkFVar fvarId }; + elabFunBinderViews (i+1) { localInsts := localInsts, .. s } + }; + if s.explicit then do + -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type); + let lctx := s.lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi; + s ← propagateExpectedType binderView.id fvar type s; + continue { lctx := lctx, .. s } + else do + mvar ← mkFreshExprMVar binderView.id type; + let lctx := s.lctx.mkLetDecl fvarId binderView.id.getId type mvar; + continue { lctx := lctx, .. s } else pure s @@ -314,6 +322,9 @@ elabFunBinders binders expectedType? explicit $ fun xs expectedType? => do { mkLambda stx xs e } +@[builtinTermElab «fun»] def elabFun : TermElab := +fun stx expectedType? => elabFunCore stx expectedType? false + /- Recall that ``` diff --git a/tests/lean/run/newfrontend5.lean b/tests/lean/run/newfrontend5.lean new file mode 100644 index 0000000000..63b6e42eb5 --- /dev/null +++ b/tests/lean/run/newfrontend5.lean @@ -0,0 +1,52 @@ +def foo {α} (f : forall {β}, β → β) (a : α) : α := +f a + +new_frontend + +#check_failure let g := id; foo g true -- fails +/- +Expands to +``` +let g : ?γ → ?γ := @id ?γ; +@foo ?α (fun (β : Sort ?u) => g) true +``` + +Unification constraint +``` + ?γ → ?γ =?= β → β +``` +fails because `β` is not in the scope of `?γ` + +Error message can be improved because it doesn't make it clear +the issue is the scope of the metavariable. Not sure yet how to improve it. +-/ +#check_failure (fun g => foo g 2) id -- fails for the same reason the previous one fail. + +#check let g := @id; foo @g true -- works +/- +Expands into +``` +let g : {γ : Sort ?v} → γ → γ := @id; +@foo ?α @g true +``` +Note that `@g` also disables implicit lambdas. +The unification constraint is easily solved +``` +{γ : Sort ?v} → γ → γ =?= {β : Sort ?u} → β → β +``` +-/ + +#check foo id true -- works +#check foo @id true -- works +#check foo (fun b => b) true -- works +#check foo (fun {β} b => b) true -- works +#check_failure foo @(fun b => b) true -- fails as expected, and error message is clear +#check foo @(fun β b => b) true -- works (implicit lambdas were disabled) +#check foo @(fun {β} b => b) true -- works (implicit lambdas were disabled) + + +set_option pp.all true + +#check let x := (fun f => (f, f)) @id; (x.1 (), x.2 true) -- works +#check_failure let x := (fun f => (f, f)) id; (x.1 (), x.2 true) -- fails as expected +#check let x := (fun (f : {α : Type} → α → α) => (f, f)) @id; (x.1 (), x.2 true) -- works