From 02e4abb24a8539b62ac3c8bfb10e3568e3252fef Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 17 Sep 2019 17:17:13 -0700 Subject: [PATCH] feat(library/init/lean/elaborator): `convertForall` skeleton --- library/init/lean/elaborator/basic.lean | 18 +++++++ library/init/lean/elaborator/preterm.lean | 62 ++++++++++++++--------- library/init/lean/elaborator/term.lean | 15 ++++-- library/init/lean/syntax.lean | 25 +++++++-- 4 files changed, 89 insertions(+), 31 deletions(-) diff --git a/library/init/lean/elaborator/basic.lean b/library/init/lean/elaborator/basic.lean index da34bb3f9e..51585166e9 100644 --- a/library/init/lean/elaborator/basic.lean +++ b/library/init/lean/elaborator/basic.lean @@ -39,6 +39,7 @@ structure ElabScope := (univs : List Name := []) (lctx : LocalContext := {}) (nextInstIdx : Nat := 1) +(inPattern : Bool := false) namespace ElabScope @@ -432,6 +433,9 @@ modifyGet $ fun s => (a, { scopes := h :: t, .. s }) | _ => (default _, s) +def localContext : Elab LocalContext := +do scope ← getScope; pure scope.lctx + def mkLocalDecl (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : Elab LocalDecl := do idx ← mkFreshName; @@ -439,6 +443,12 @@ modifyGetScope $ fun scope => let (decl, lctx) := scope.lctx.mkLocalDecl idx userName type bi; (decl, { lctx := lctx, .. scope }) +def mkLambda (xs : Array Expr) (b : Expr) : Elab Expr := +do lctx ← localContext; pure $ lctx.mkLambda xs b + +def mkForall (xs : Array Expr) (b : Expr) : Elab Expr := +do lctx ← localContext; pure $ lctx.mkForall xs b + def anonymousInstNamePrefix := `_inst def mkAnonymousInstName : Elab Name := @@ -489,6 +499,14 @@ a ← x; modify $ fun s => { scopes := s.scopes.tail, .. s}; pure a +@[inline] def withInPattern {α} (x : Elab α) : Elab α := +withNewScope $ do + modifyScope $ fun scope => { inPattern := true, .. scope }; + x + +def inPattern : Elab Bool := +do scope ← getScope; pure $ scope.inPattern + /- Remark: in an ideal world where performance doesn't matter, we would define `Elab` as ``` ExceptT ElabException (StateT ElabException IO) diff --git a/library/init/lean/elaborator/preterm.lean b/library/init/lean/elaborator/preterm.lean index 268a456f1d..6d5e08cb77 100644 --- a/library/init/lean/elaborator/preterm.lean +++ b/library/init/lean/elaborator/preterm.lean @@ -56,6 +56,9 @@ private def dummy : Expr := Expr.const `Prop [] def mkAsIs (e : Expr) : PreTerm := e.mkAnnotation `as_is +def mkAsPattern (id : Name) (e : PreTerm) : PreTerm := +(Expr.app (Expr.fvar id) e).mkAnnotation `as_pattern + def mkPreTypeAscription (p : PreTerm) (expectedType : Expr) : PreTerm := Expr.app (Expr.app (Expr.const `typedExpr []) expectedType) p @@ -138,23 +141,38 @@ fun n => do private def mkLocal (decl : LocalDecl) : PreTerm := Expr.local decl.name decl.userName decl.type decl.binderInfo -private def processBinder (b : Syntax Expr) : Elab (List PreTerm) := +private def processBinder (b : Syntax Expr) : Elab (Array PreTerm) := match b.getKind with | `Lean.Parser.Term.simpleBinder => do let args := (b.getArg 0).getArgs; - args.mfoldl (fun r arg => do + args.mmap $ fun arg => do let id := arg.getId; hole ← mkHoleFor arg; decl ← mkLocalDecl id hole; - pure (mkLocal decl :: r)) - [] -| `Lean.Parser.Term.explicitBinder => do runIO (IO.println $ ">> explicit " ++ (toString b)); pure [] -| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure [] -| `Lean.Parser.Term.instBinder => do runIO (IO.println $ ">> inst " ++ (toString b)); pure [] + pure (mkLocal decl) +| `Lean.Parser.Term.explicitBinder => + let ids := (b.getArg 1).getArgs; + let optType := b.getArg 2; + let optDef := b.getArg 3; + ids.mmap $ fun idStx => do + let id := idStx.getId; + type ← if optType.getNumArgs == 0 then mkHoleFor idStx else toPreTerm (optType.getArg 1); + type ← if optDef.getNumArgs == 0 then pure type else + let defInfo := optDef.getArg 0; + match defInfo.getKind with + | `Lean.Parser.Term.binderDefault => do + defVal ← toPreTerm (defInfo.getArg 1); + pure $ Expr.app (Expr.app (Expr.const `optParam []) type) defVal + | `Lean.Parser.Term.binderTactic => logErrorAndThrow optDef "old elaborator does not support tactics in parameters" + | _ => throw "unknown binder default value annotation"; + decl ← mkLocalDecl id type; + pure (mkLocal decl) +| `Lean.Parser.Term.implicitBinder => do runIO (IO.println $ ">> implict " ++ (toString b)); pure Array.empty +| `Lean.Parser.Term.instBinder => do runIO (IO.println $ ">> inst " ++ (toString b)); pure Array.empty | _ => throw "unknown binder kind" -private def processBinders (bs : Array (Syntax Expr)) : Elab (List PreTerm) := -bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) [] +private def processBinders (bs : Array (Syntax Expr)) : Elab (Array PreTerm) := +bs.mfoldl (fun r s => do xs ← processBinder s; pure (r ++ xs)) Array.empty @[builtinPreTermElab «forall»] def convertForall : PreTermElab := fun n => do @@ -162,21 +180,8 @@ fun n => do let body := n.getArg 3; withNewScope $ do xs ← processBinders binders.getArgs; - runIO (IO.println (xs.map Expr.dbgToString)); body ← toPreTerm body; - -- TODO - pure $ Expr.sort (Level.zero) --- dom ← toPreTerm $ n.getArg 0; --- rng ← toPreTerm $ n.getArg 2; --- pure $ Expr.pi id BinderInfo.default dom rng - --- TODO: delete... arrow should be expanded at term.lean -@[builtinPreTermElab «arrow»] def convertArrow : PreTermElab := -fun n => do - id ← mkFreshName; - dom ← toPreTerm $ n.getArg 0; - rng ← toPreTerm $ n.getArg 2; - pure $ Expr.pi id BinderInfo.default dom rng + mkForall xs body @[builtinPreTermElab «hole»] def convertHole : PreTermElab := fun _ => pure $ Expr.mvar Name.anonymous @@ -184,6 +189,17 @@ fun _ => pure $ Expr.mvar Name.anonymous @[builtinPreTermElab «sorry»] def convertSorry : PreTermElab := fun _ => pure $ Expr.app (Expr.const `sorryAx []) (Expr.mvar Name.anonymous) +@[builtinPreTermElab «id»] def convertId : PreTermElab := +fun n => do + let id := n.getIdAt 0; + -- TODO add support for `explicitUniv` and `namedPattern` + lctx ← localContext; + match lctx.findFromUserName id with + | some decl => pure $ mkLocal decl + | none => + -- TODO global name resolution + logErrorAndThrow n.val ("unknown identifier '" ++ toString id ++ "'") + def oldElaborate (stx : Syntax Expr) (expectedType : Option Expr := none) : Elab Expr := do p ← toPreTerm stx; diff --git a/library/init/lean/elaborator/term.lean b/library/init/lean/elaborator/term.lean index 94cc9e8533..4c42e9bc1a 100644 --- a/library/init/lean/elaborator/term.lean +++ b/library/init/lean/elaborator/term.lean @@ -49,15 +49,20 @@ fun stx _ => do let openBkt := stx.getArg 0; let args := stx.getArg 1; let closeBkt := stx.getArg 2; - let consId := openBkt.mkIdent `List.cons; - let nilId := closeBkt.mkIdent `List.nil; + let consId := mkIdentFrom openBkt `List.cons; + let nilId := mkIdentFrom closeBkt `List.nil; pure $ args.foldSepArgs (fun arg r => mkAppStx consId [arg, r]) nilId +def mkExplicitBinder {α} (n : Syntax α) (type : Syntax α) : Syntax α := +mkNode `Lean.Parser.Term.explicitBinder [mkAtom "(", mkNullNode [n], mkNullNode [mkAtom ":", type], mkNullNode [], mkAtom ")"] + @[builtinTermElab arrow] def elabArrow : TermElab := fun stx _ => do - id ← mkFreshName; - runIO (IO.println stx.val); - pure $ Syntax.other $ Expr.sort (Level.zero) + n ← mkFreshName; + let id := mkIdentFrom stx.val n; + let dom := stx.getArg 0; + let rng := stx.getArg 2; + pure $ mkNode `Lean.Parser.Term.forall [mkAtom "forall", mkNullNode [mkExplicitBinder id dom], mkAtom ",", rng] end Elab end Lean diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean index 95afdcf2d3..bec55aa31e 100644 --- a/library/init/lean/syntax.lean +++ b/library/init/lean/syntax.lean @@ -329,7 +329,7 @@ end SyntaxNode /- Helper functions for creating Syntax objects using C++ -/ @[export lean_mk_syntax_atom] -def mkSimpleAtom (val : String) : Syntax := +def mkSimpleAtomCore (val : String) : Syntax := Syntax.atom none val @[export lean_mk_syntax_ident] @@ -340,6 +340,20 @@ Syntax.ident none (toString val).toSubstring val [] def mkListNode (args : Array Syntax) : Syntax := Syntax.node nullKind args +def mkAtom {α} (val : String) : Syntax α := +Syntax.atom none val + +@[inline] def mkNode {α} (k : SyntaxNodeKind) (args : List (Syntax α)) : Syntax α := +Syntax.node k args.toArray + +@[inline] def mkNullNode {α} (args : List (Syntax α)) : Syntax α := +Syntax.node nullKind args.toArray + +def mkOptionalNode {α} (arg : Option (Syntax α)) : Syntax α := +match arg with +| some arg => Syntax.node nullKind (Array.singleton arg) +| none => Syntax.node nullKind Array.empty + /- Helper functions for creating string and numeric literals -/ def mkLit (kind : SyntaxNodeKind) (val : String) (info : Option SourceInfo := none) : Syntax := @@ -457,10 +471,15 @@ match stx.isNatLit with | some val => val | none => 0 +end Syntax + /-- Create an identifier using `SourceInfo` from `src` -/ -def mkIdent {α} (src : Syntax α) (val : Name) : Syntax α := +def mkIdentFrom {α} (src : Syntax α) (val : Name) : Syntax α := let info := src.getHeadInfo; Syntax.ident info (toString val).toSubstring val [] -end Syntax +def mkAtomFrom {α} (src : Syntax α) (val : String) : Syntax α := +let info := src.getHeadInfo; +Syntax.atom info val + end Lean