From fddeecaaa66e85f67ed0be3001b1294c7b89db4d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 8 Dec 2019 17:59:11 -0800 Subject: [PATCH] feat: elaborate binders --- src/Init/Lean/Elab/Command.lean | 64 +++++++++---- src/Init/Lean/Elab/Term.lean | 161 +++++++++++++++++++++++++++++--- src/Init/Lean/Syntax.lean | 4 +- tests/lean/run/frontend1.lean | 10 +- 4 files changed, 203 insertions(+), 36 deletions(-) diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean index 50cc413971..e374030250 100644 --- a/src/Init/Lean/Elab/Command.lean +++ b/src/Init/Lean/Elab/Command.lean @@ -24,7 +24,7 @@ structure Scope := (ns : Name := Name.anonymous) -- current namespace (openDecls : List OpenDecl := []) (univNames : List Name := []) -(varDecls : List Syntax := []) +(varDecls : Array Syntax := #[]) instance Scope.inhabited : Inhabited Scope := ⟨{ kind := "", header := "" }⟩ @@ -95,25 +95,33 @@ stx.ifNode | none => logError stx ("command '" ++ toString k ++ "' has not been implemented")) (fun _ => logErrorUsingCmdPos ("unexpected command")) -@[specialize] def runTermElabM {α} (x : TermElabM α) : CommandElabM α := -fun ctx s => - let scope := s.scopes.head!; - let termCtx : Term.Context := { - config := { opts := scope.options, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true }, - fileName := ctx.fileName, - fileMap := ctx.fileMap, - cmdPos := s.cmdPos, - ns := scope.ns, - univNames := scope.univNames, - openDecls := scope.openDecls - }; - let termState : Term.State := { - env := s.env, - messages := s.messages - }; - match (tracingAtPos s.cmdPos x) termCtx termState with - | EStateM.Result.ok a newS => EStateM.Result.ok a { env := newS.env, messages := newS.messages, .. s } - | EStateM.Result.error ex newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s } +private def mkTermContext (ctx : Context) (s : State) : Term.Context := +let scope := s.scopes.head!; +{ config := { opts := scope.options, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true }, + fileName := ctx.fileName, + fileMap := ctx.fileMap, + cmdPos := s.cmdPos, + ns := scope.ns, + univNames := scope.univNames, + openDecls := scope.openDecls } + +private def mkTermState (s : State) : Term.State := +{ env := s.env, + messages := s.messages } + +private def getVarDecls (s : State) : Array Syntax := +s.scopes.head!.varDecls + +private def toCommandResult {α} (s : State) (result : EStateM.Result Exception Term.State α) : EStateM.Result Exception State α := +match result with +| EStateM.Result.ok a newS => EStateM.Result.ok a { env := newS.env, messages := newS.messages, .. s } +| EStateM.Result.error ex newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s } + +@[inline] def runTermElabM {α} (x : TermElabM α) : CommandElabM α := +fun ctx s => toCommandResult s $ tracingAtPos s.cmdPos (Term.elabBinders (getVarDecls s) x) (mkTermContext ctx s) (mkTermState s) + +def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit := +_root_.dbgTrace (toString a) $ fun _ => pure () def getEnv : CommandElabM Environment := do s ← get; pure s.env @@ -323,6 +331,22 @@ fun n => do @[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure () @[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure () +@[builtinCommandElab «variable»] def elabVariable : CommandElab := +fun n => do + -- `variable` bracktedBinder + let binder := n.getArg 1; + -- Try to elaborate `binder` for sanity checking + runTermElabM $ Term.elabBinder binder $ pure (); + modifyScope $ fun scope => { varDecls := scope.varDecls.push binder, .. scope } + +@[builtinCommandElab «variables»] def elabVariables : CommandElab := +fun n => do + -- `variables` bracktedBinder+ + let binders := (n.getArg 1).getArgs; + -- Try to elaborate `binders` for sanity checking + runTermElabM $ Term.elabBinders binders $ pure (); + modifyScope $ fun scope => { varDecls := scope.varDecls ++ binders, .. scope } + end Command /- diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean index d7d3e4a89b..d28ce27928 100644 --- a/src/Init/Lean/Elab/Term.lean +++ b/src/Init/Lean/Elab/Term.lean @@ -27,9 +27,11 @@ inductive SyntheticMVarInfo | postponed (macroStack : List Syntax) : SyntheticMVarInfo structure State extends Meta.State := -(macroStack : List Syntax := []) -(syntheticMVars : List (MVarId × SyntheticMVarInfo) := []) -(messages : MessageLog := {}) +(macroStack : List Syntax := []) +(syntheticMVars : List (MVarId × SyntheticMVarInfo) := []) +(messages : MessageLog := {}) +(instImplicitIdx : Nat := 1) +(anonymousIdx : Nat := 1) abbrev TermElabM := ReaderT Context (EStateM Exception State) abbrev TermElab := SyntaxNode → Option Expr → TermElabM Expr @@ -86,6 +88,8 @@ fun ctx s => match x ctx.toContext s.toState with | EStateM.Result.ok a newS => EStateM.Result.ok a { toState := newS, .. s } | EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s } +def getLCtx : TermElabM LocalContext := do ctx ← read; pure ctx.lctx +def getLocalInsts : TermElabM LocalInstances := do ctx ← read; pure ctx.localInstances def getOptions : TermElabM Options := do ctx ← read; pure ctx.config.opts def getTraceState : TermElabM TraceState := do s ← get; pure s.traceState def setTraceState (traceState : TraceState) : TermElabM Unit := modify $ fun s => { traceState := traceState, .. s } @@ -106,24 +110,28 @@ _root_.dbgTrace (toString a) $ fun _ => pure () def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.isDefEq t s def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e +def isClass (t : Expr) : TermElabM (Option Name) := liftMetaM $ Meta.isClass t def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar def mkFreshExprMVar (type : Expr) (userName? : Name := Name.anonymous) (synthetic : Bool := false) : TermElabM Expr := liftMetaM $ Meta.mkFreshExprMVar type userName? synthetic +@[inline] def withNode {α} (stx : Syntax) (x : SyntaxNode → TermElabM α) : TermElabM α := +stx.ifNode x (fun _ => throw $ Exception.other "term elaborator failed, unexpected syntax") + def elabTerm (stx : Syntax) (expectedType : Option Expr) : TermElabM Expr := -stx.ifNode - (fun n => do - s ← get; - let tables := termElabAttribute.ext.getState s.env; - let k := n.getKind; - match tables.find k with - | some elab => tracingAt stx $ elab n expectedType - | none => throw $ Exception.other ("elaboration function for '" ++ toString k ++ "' has not been implemented")) - (fun _ => throw $ Exception.other "term elaborator failed, unexpected syntax") +withNode stx $ fun node => do + s ← get; + let tables := termElabAttribute.ext.getState s.env; + let k := node.getKind; + match tables.find k with + | some elab => tracingAt stx $ elab node expectedType + | none => throw $ Exception.other ("elaboration function for '" ++ toString k ++ "' has not been implemented") def elabType (stx : Syntax) : TermElabM Expr := do u ← mkFreshLevelMVar; - elabTerm stx (mkSort u) + type ← elabTerm stx (mkSort u); + -- TODO: ensure it is a type + pure type @[builtinTermElab «prop»] def elabProp : TermElab := fun _ _ => pure $ mkSort levelZero @@ -134,6 +142,133 @@ fun _ _ => pure $ mkSort levelZero @[builtinTermElab «type»] def elabTypeStx : TermElab := fun _ _ => pure $ mkSort levelOne +@[builtinTermElab «hole»] def elabHole : TermElab := +fun _ expectedType? => + match expectedType? with + | some expectedType => mkFreshExprMVar expectedType + | none => do u ← mkFreshLevelMVar; mkFreshExprMVar (mkSort u) + +private def mkFreshAnonymousName : TermElabM Name := +do s ← get; + let anonymousIdx := s.anonymousIdx; + modify $ fun s => { anonymousIdx := s.anonymousIdx + 1, .. s}; + pure $ (`_a).appendIndexAfter anonymousIdx + +private def mkFreshInstanceName : TermElabM Name := +do s ← get; + let instIdx := s.instImplicitIdx; + modify $ fun s => { instImplicitIdx := s.instImplicitIdx + 1, .. s}; + pure $ (`_inst).appendIndexAfter instIdx + +def mkHole := mkNode `Lean.Parser.Term.hole [mkAtom "_"] + +/-- Given syntax of the form (`:` term)?, return `term` if it is present, and a hole otherwise. -/ +private def expandOptType (stx : Syntax) : Syntax := +if stx.getNumArgs == 0 then + mkHole +else + stx.getArg 1 + +/-- Given syntax of the form `ident <|> hole`, return `ident`. If `hole`, then we create a new anonymous name. -/ +private def expandBinderIdent (stx : Syntax) : TermElabM Syntax := +if stx.getKind == `Lean.Parser.Term.hole then do + id ← mkFreshAnonymousName; + pure $ mkIdentFrom stx id +else + pure stx + +/-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/ +private def expandOptIdent (stx : Syntax) : TermElabM Syntax := +if stx.getNumArgs == 0 then do + id ← mkFreshInstanceName; pure $ mkIdentFrom stx id +else + pure $ stx.getArg 0 + +structure BinderView := +(id : Syntax) (type : Syntax) (bi : BinderInfo) + +private def matchBinder (stx : Syntax) : TermElabM (Array BinderView) := +withNode stx $ fun node => do + let k := node.getKind; + if k == `Lean.Parser.Term.simpleBinder then + -- binderIdent+ + let ids := (node.getArg 0).getArgs; + let type := mkHole; + ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default } + else if k == `Lean.Parser.Term.explicitBinder then + -- `(` binderIdent+ (`:` type)? (binderDefault <|> binderTactic)? `)` + let ids := (node.getArg 1).getArgs; + let type := expandOptType (node.getArg 2); + -- TODO handle `binderDefault` and `binderTactic` + ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.default } + else if k == `Lean.Parser.Term.implicitBinder then + -- `{` binderIdent+ (`:` type)? `}` + let ids := (node.getArg 1).getArgs; + let type := expandOptType (node.getArg 2); + ids.mapM $ fun id => do id ← expandBinderIdent id; pure { id := id, type := type, bi := BinderInfo.implicit } + else if k == `Lean.Parser.Term.instBinder then do + -- `[` optIdent type `]` + id ← expandOptIdent (node.getArg 1); + let type := node.getArg 2; + pure #[ { id := id, type := type, bi := BinderInfo.instImplicit } ] + else + throw $ Exception.other "term elaborator failed, unexpected binder syntax" + +@[inline] def withLCtx {α} (lctx : LocalContext) (localInsts : LocalInstances) (x : TermElabM α) : TermElabM α := +adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := localInsts, .. ctx }) x + +def resetSynthInstanceCache : TermElabM Unit := +modify $ fun s => { cache := { synthInstance := {}, .. s.cache }, .. s } + +@[inline] def resettingSynthInstanceCache {α} (x : TermElabM α) : TermElabM α := +do s ← get; + let savedSythInstance := s.cache.synthInstance; + resetSynthInstanceCache; + finally x (modify $ fun s => { cache := { synthInstance := savedSythInstance, .. s.cache }, .. s }) + +@[inline] def resettingSynthInstanceCacheWhen {α} (b : Bool) (x : TermElabM α) : TermElabM α := +if b then resettingSynthInstanceCache x else x + +def mkFreshId : TermElabM Name := +do s ← get; + let id := s.ngen.curr; + modify $ fun s => { ngen := s.ngen.next, .. s }; + pure id + +private partial def elabBindersAux (binders : Array Syntax) : Nat → LocalContext → LocalInstances → TermElabM (LocalContext × LocalInstances) +| i, lctx, localInsts => + if h : i < binders.size then do + binderViews ← matchBinder (binders.get ⟨i, h⟩); + (lctx, localInsts) ← binderViews.foldlM + (fun (p : LocalContext × LocalInstances) binderView => do + let (lctx, localInsts) := p; + withLCtx lctx localInsts $ do + type ← elabType binderView.type; + fvarId ← mkFreshId; + -- dbgTrace (toString binderView.id.getId ++ " : " ++ toString type); + let lctx := lctx.mkLocalDecl fvarId binderView.id.getId type binderView.bi; + className? ← isClass type; + match className? with + | none => pure (lctx, localInsts) + | some className => do + resetSynthInstanceCache; + let localInsts := localInsts.push { className := className, fvar := mkFVar fvarId }; + pure (lctx, localInsts)) + (lctx, localInsts); + elabBindersAux (i+1) lctx localInsts + else + pure (lctx, localInsts) + +@[inline] def elabBinders {α} (binders : Array Syntax) (x : TermElabM α) : TermElabM α := +do lctx ← getLCtx; + localInsts ← getLocalInsts; + (lctx, newLocalInsts) ← elabBindersAux binders 0 lctx localInsts; + resettingSynthInstanceCacheWhen (newLocalInsts.size > localInsts.size) $ + adaptReader (fun (ctx : Context) => { lctx := lctx, localInstances := newLocalInsts, .. ctx }) x + +@[inline] def elabBinder {α} (binder : Syntax) (x : TermElabM α) : TermElabM α := +elabBinders #[binder] x + end Term export Term (TermElabM) diff --git a/src/Init/Lean/Syntax.lean b/src/Init/Lean/Syntax.lean index 1e92a232ea..3f44677024 100644 --- a/src/Init/Lean/Syntax.lean +++ b/src/Init/Lean/Syntax.lean @@ -331,10 +331,10 @@ Syntax.node nullKind args def mkAtom (val : String) : Syntax := Syntax.atom none val -@[inline] def mkNode (k : SyntaxNodeKind) (args : List (Syntax)) : Syntax := +@[inline] def mkNode (k : SyntaxNodeKind) (args : List Syntax) : Syntax := Syntax.node k args.toArray -@[inline] def mkNullNode (args : List (Syntax)) : Syntax := +@[inline] def mkNullNode (args : List Syntax) : Syntax := Syntax.node nullKind args.toArray def mkOptionalNode (arg : Option Syntax) : Syntax := diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean index bb699f5dac..959e29457a 100644 --- a/tests/lean/run/frontend1.lean +++ b/tests/lean/run/frontend1.lean @@ -7,4 +7,12 @@ do (env, messages) ← testFrontend input; messages.toList.forM $ fun msg => IO.println msg; pure () -#eval run "import Init.Core universe u universe v section namespace foo.bla end bla end foo end" +#eval run +"import Init.Core + universe u universe v + section namespace foo.bla end bla end foo + variable (p q : Prop) + variable (_ b : _) + variable {α : Type} + -- variable [Monad m] + end"