chore: remove tmp dir
This commit is contained in:
Leonardo de Moura
parent
b1a92f5cbf
commit
e7dd03d5d1
25 changed files with 0 additions and 7503 deletions
469
tmp/Basic.lean
469
tmp/Basic.lean
|
|
@ -1,469 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2019 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
-/
|
||||
prelude
|
||||
import Init.Control.Reader
|
||||
import Init.Lean.Meta
|
||||
import Init.Lean.Parser.Module
|
||||
|
||||
namespace Lean
|
||||
namespace Elab
|
||||
|
||||
/-
|
||||
structure ElabContext :=
|
||||
(fileName : String)
|
||||
(fileMap : FileMap)
|
||||
|
||||
structure ElabScope :=
|
||||
(cmd : String)
|
||||
(header : Name)
|
||||
(options : Options := {})
|
||||
(ns : Name := Name.anonymous) -- current namespace
|
||||
(openDecls : List OpenDecl := [])
|
||||
(univs : List Name := [])
|
||||
(lctx : LocalContext := {})
|
||||
(nextInstIdx : Nat := 1)
|
||||
(inPattern : Bool := false)
|
||||
|
||||
namespace ElabScope
|
||||
|
||||
instance : Inhabited ElabScope := ⟨{ cmd := "", header := arbitrary _ }⟩
|
||||
|
||||
end ElabScope
|
||||
|
||||
structure ElabState :=
|
||||
(env : Environment)
|
||||
(messages : MessageLog := {})
|
||||
(cmdPos : String.Pos := 0)
|
||||
(ngen : NameGenerator := {})
|
||||
(mctx : MetavarContext := {})
|
||||
(scopes : List ElabScope := [{ cmd := "root", header := Name.anonymous }])
|
||||
|
||||
inductive ElabException
|
||||
| io : IO.Error → ElabException
|
||||
| msg : Message → ElabException
|
||||
| kernel : KernelException → ElabException
|
||||
| other : String → ElabException
|
||||
/- ElabException.silent is used when we log an error in `messages`, and then
|
||||
want to interrupt the elaborator execution. We use it to make sure the
|
||||
top-level handler does not record it again in `messages`. See `logErrorAndThrow` -/
|
||||
| silent : ElabException
|
||||
|
||||
namespace ElabException
|
||||
|
||||
instance : Inhabited ElabException := ⟨other "error"⟩
|
||||
|
||||
end ElabException
|
||||
|
||||
abbrev Elab := ReaderT ElabContext (EStateM ElabException ElabState)
|
||||
|
||||
instance str2ElabException : HasCoe String ElabException := ⟨ElabException.other⟩
|
||||
|
||||
abbrev TermElab := SyntaxNode Expr → Option Expr → Elab (Syntax Expr)
|
||||
abbrev CommandElab := SyntaxNode → Elab Unit
|
||||
|
||||
abbrev TermElabTable : Type := SMap SyntaxNodeKind TermElab
|
||||
abbrev CommandElabTable : Type := SMap SyntaxNodeKind CommandElab
|
||||
def mkBuiltinTermElabTable : IO (IO.Ref TermElabTable) := IO.mkRef {}
|
||||
def mkBuiltinCommandElabTable : IO (IO.Ref CommandElabTable) := IO.mkRef {}
|
||||
@[init mkBuiltinTermElabTable]
|
||||
constant builtinTermElabTable : IO.Ref TermElabTable := arbitrary _
|
||||
@[init mkBuiltinCommandElabTable]
|
||||
constant builtinCommandElabTable : IO.Ref CommandElabTable := arbitrary _
|
||||
|
||||
def addBuiltinTermElab (k : SyntaxNodeKind) (declName : Name) (elab : TermElab) : IO Unit :=
|
||||
do m ← builtinTermElabTable.get;
|
||||
when (m.contains k) $
|
||||
throw (IO.userError ("invalid builtin term elaborator, elaborator for '" ++ toString k ++ "' has already been defined"));
|
||||
builtinTermElabTable.modify $ fun m => m.insert k elab
|
||||
|
||||
def addBuiltinCommandElab (k : SyntaxNodeKind) (declName : Name) (elab : CommandElab) : IO Unit :=
|
||||
do m ← builtinCommandElabTable.get;
|
||||
when (m.contains k) $
|
||||
throw (IO.userError ("invalid builtin command elaborator, elaborator for '" ++ toString k ++ "' has already been defined"));
|
||||
builtinCommandElabTable.modify $ fun m => m.insert k elab
|
||||
|
||||
def checkSyntaxNodeKind (k : Name) : IO Name :=
|
||||
do b ← Parser.isValidSyntaxNodeKind k;
|
||||
if b then pure k
|
||||
else throw (IO.userError "failed")
|
||||
|
||||
def checkSyntaxNodeKindAtNamespaces (k : Name) : List Name → IO Name
|
||||
| [] => throw (IO.userError "failed")
|
||||
| n::ns => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces ns
|
||||
|
||||
def syntaxNodeKindOfAttrParam (env : Environment) (parserNamespace : Name) (arg : Syntax) : IO SyntaxNodeKind :=
|
||||
match attrParamSyntaxToIdentifier arg with
|
||||
| some k =>
|
||||
checkSyntaxNodeKind k
|
||||
<|>
|
||||
checkSyntaxNodeKindAtNamespaces k env.getNamespaces
|
||||
<|>
|
||||
checkSyntaxNodeKind (parserNamespace ++ k)
|
||||
<|>
|
||||
throw (IO.userError ("invalid syntax node kind '" ++ toString k ++ "'"))
|
||||
| none => throw (IO.userError ("syntax node kind is missing"))
|
||||
|
||||
def declareBuiltinElab (env : Environment) (addFn : Name) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
|
||||
let name := `_regBuiltinTermElab ++ declName;
|
||||
let type := mkApp (mkConst `IO) (mkConst `Unit);
|
||||
let val := mkAppN (mkConst addFn) #[toExpr kind, toExpr declName, mkConst declName];
|
||||
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
|
||||
match env.addAndCompile {} decl with
|
||||
-- TODO: pretty print error
|
||||
| Except.error _ => throw (IO.userError ("failed to emit registration code for builtin term elaborator '" ++ toString declName ++ "'"))
|
||||
| Except.ok env => IO.ofExcept (setInitAttr env name)
|
||||
|
||||
def declareBuiltinTermElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
|
||||
declareBuiltinElab env `Lean.addBuiltinTermElab kind declName
|
||||
|
||||
def declareBuiltinCommandElab (env : Environment) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
|
||||
declareBuiltinElab env `Lean.addBuiltinCommandElab kind declName
|
||||
|
||||
@[init] def registerBuiltinTermElabAttr : IO Unit :=
|
||||
registerAttribute {
|
||||
name := `builtinTermElab,
|
||||
descr := "Builtin term elaborator",
|
||||
add := fun env declName arg persistent => do {
|
||||
unless persistent $ throw (IO.userError ("invalid attribute 'builtinTermElab', must be persistent"));
|
||||
kind ← syntaxNodeKindOfAttrParam env `Lean.Parser.Term arg;
|
||||
match env.find declName with
|
||||
| none => throw "unknown declaration"
|
||||
| some decl =>
|
||||
match decl.type with
|
||||
| Expr.const `Lean.TermElab _ _ => declareBuiltinTermElab env kind declName
|
||||
| _ => throw (IO.userError ("unexpected term elaborator type at '" ++ toString declName ++ "' `TermElab` expected"))
|
||||
},
|
||||
applicationTime := AttributeApplicationTime.afterCompilation
|
||||
}
|
||||
|
||||
@[init] def registerBuiltinCommandElabAttr : IO Unit :=
|
||||
registerAttribute {
|
||||
name := `builtinCommandElab,
|
||||
descr := "Builtin command elaborator",
|
||||
add := fun env declName arg persistent => do {
|
||||
unless persistent $ throw (IO.userError ("invalid attribute 'builtinCommandElab', must be persistent"));
|
||||
kind ← syntaxNodeKindOfAttrParam env `Lean.Parser.Command arg;
|
||||
match env.find declName with
|
||||
| none => throw "unknown declaration"
|
||||
| some decl =>
|
||||
match decl.type with
|
||||
| Expr.const `Lean.CommandElab _ _ => declareBuiltinCommandElab env kind declName
|
||||
| _ => throw (IO.userError ("unexpected command elaborator type at '" ++ toString declName ++ "' `CommandElab` expected"))
|
||||
},
|
||||
applicationTime := AttributeApplicationTime.afterCompilation
|
||||
}
|
||||
|
||||
structure ElabAttributeEntry :=
|
||||
(kind : SyntaxNodeKind)
|
||||
(declName : Name)
|
||||
|
||||
structure ElabAttribute (σ : Type) :=
|
||||
(attr : AttributeImpl)
|
||||
(ext : PersistentEnvExtension ElabAttributeEntry σ)
|
||||
(kind : String)
|
||||
|
||||
namespace ElabAttribute
|
||||
|
||||
instance {σ} [Inhabited σ] : Inhabited (ElabAttribute σ) := ⟨{ attr := arbitrary _, ext := arbitrary _, kind := "" }⟩
|
||||
|
||||
end ElabAttribute
|
||||
|
||||
/-
|
||||
This is just the basic skeleton for the `[termElab]` attribute and environment extension.
|
||||
The state is initialized using `builtinTermElabTable`.
|
||||
|
||||
The current implementation just uses the bultin elaborators.
|
||||
-/
|
||||
def mkElabAttribute {σ} [Inhabited σ] (attrName : Name) (kind : String) (builtinTable : IO.Ref σ) : IO (ElabAttribute σ) :=
|
||||
do ext : PersistentEnvExtension ElabAttributeEntry σ ← registerPersistentEnvExtension {
|
||||
name := attrName,
|
||||
addImportedFn := fun es => do
|
||||
table ← builtinTable.get;
|
||||
-- TODO: populate table with `es`
|
||||
pure table,
|
||||
addEntryFn := fun (s : σ) _ => s, -- TODO
|
||||
exportEntriesFn := fun _ => #[], -- TODO
|
||||
statsFn := fun _ => fmt (kind ++ " elaborator attribute") -- TODO
|
||||
};
|
||||
let attrImpl : AttributeImpl := {
|
||||
name := attrName,
|
||||
descr := kind ++ " elaborator",
|
||||
add := fun env decl args persistent => pure env -- TODO
|
||||
};
|
||||
pure { ext := ext, attr := attrImpl, kind := kind }
|
||||
|
||||
abbrev TermElabAttribute := ElabAttribute TermElabTable
|
||||
def mkTermElabAttribute : IO TermElabAttribute :=
|
||||
mkElabAttribute `elabTerm "term" builtinTermElabTable
|
||||
@[init mkTermElabAttribute]
|
||||
constant termElabAttribute : TermElabAttribute := arbitrary _
|
||||
|
||||
abbrev CommandElabAttribute := ElabAttribute CommandElabTable
|
||||
def mkCommandElabAttribute : IO CommandElabAttribute :=
|
||||
mkElabAttribute `commandTerm "command" builtinCommandElabTable
|
||||
@[init mkCommandElabAttribute]
|
||||
constant commandElabAttribute : CommandElabAttribute := arbitrary _
|
||||
|
||||
namespace Elab
|
||||
def logMessage (msg : Message) : Elab Unit :=
|
||||
modify $ fun s => { messages := s.messages.add msg, .. s }
|
||||
|
||||
def getPosition (pos : Option String.Pos := none) : Elab Position :=
|
||||
do ctx ← read;
|
||||
s ← get;
|
||||
pure $ ctx.fileMap.toPosition (pos.getD s.cmdPos)
|
||||
|
||||
def mkMessage (msg : String) (pos : Option String.Pos := none) : Elab Message :=
|
||||
do ctx ← read;
|
||||
s ← get;
|
||||
let pos := ctx.fileMap.toPosition (pos.getD s.cmdPos);
|
||||
pure { fileName := ctx.fileName, pos := pos, data := msg }
|
||||
|
||||
def logErrorAt (pos : String.Pos) (errorMsg : String) : Elab Unit :=
|
||||
mkMessage errorMsg pos >>= logMessage
|
||||
|
||||
def logErrorUsingCmdPos (errorMsg : String) : Elab Unit :=
|
||||
do s ← get;
|
||||
logErrorAt s.cmdPos errorMsg
|
||||
|
||||
def getPos {α} (stx : Syntax α) : Elab String.Pos :=
|
||||
match stx.getPos with
|
||||
| some p => pure p
|
||||
| none => do s ← get; pure s.cmdPos
|
||||
|
||||
def logError {α} (stx : Syntax α) (errorMsg : String) : Elab Unit :=
|
||||
do pos ← getPos stx;
|
||||
logErrorAt pos errorMsg
|
||||
|
||||
def logElabException (e : ElabException) : Elab Unit :=
|
||||
let log (msg : Message) : Elab Unit :=
|
||||
modify $ fun s => { messages := s.messages.add msg, .. s };
|
||||
match e with
|
||||
| ElabException.silent => pure () -- do nothing since message was already logged
|
||||
| ElabException.msg m => log m
|
||||
| ElabException.io e => mkMessage (toString e) >>= log
|
||||
| ElabException.other e => mkMessage e >>= log
|
||||
| ElabException.kernel e =>
|
||||
match e with
|
||||
| KernelException.other msg => mkMessage msg >>= log
|
||||
| _ => mkMessage "kernel exception" >>= log -- TODO(pretty print them)
|
||||
|
||||
def logErrorAndThrow {α β : Type} (stx : Syntax β) (errorMsg : String) : Elab α :=
|
||||
do logError stx errorMsg;
|
||||
throw ElabException.silent
|
||||
|
||||
def logUnknownDecl {α} (stx : Syntax α) (declName : Name) : Elab Unit :=
|
||||
logError stx ("unknown declaration '" ++ toString declName ++ "'")
|
||||
|
||||
def getEnv : Elab Environment :=
|
||||
do s ← get; pure s.env
|
||||
|
||||
def setEnv (env : Environment) : Elab Unit :=
|
||||
modify $ fun s => { env := env, .. s }
|
||||
|
||||
def elabCommand (stx : Syntax) : Elab Unit :=
|
||||
stx.ifNode
|
||||
(fun n => do
|
||||
s ← get;
|
||||
let tables := commandElabAttribute.ext.getState s.env;
|
||||
let k := n.getKind;
|
||||
match tables.find k with
|
||||
| some elab => elab n
|
||||
| none => logError stx ("command '" ++ toString k ++ "' has not been implemented"))
|
||||
(fun _ => logErrorUsingCmdPos ("unexpected command"))
|
||||
-/
|
||||
|
||||
structure ElabContext :=
|
||||
(fileName : String)
|
||||
(fileMap : FileMap)
|
||||
|
||||
inductive ElabException
|
||||
| io : IO.Error → ElabException
|
||||
| msg : Message → ElabException
|
||||
| kernel : KernelException → ElabException
|
||||
|
||||
structure ElabState :=
|
||||
(dummy : Unit := ())
|
||||
|
||||
structure FrontendState :=
|
||||
(elabState : ElabState)
|
||||
(parserState : Parser.ModuleParserState)
|
||||
|
||||
abbrev Frontend := ReaderT Parser.ParserContextCore (EStateM ElabException FrontendState)
|
||||
|
||||
/-
|
||||
def getElabContext : Frontend ElabContext :=
|
||||
do c ← read;
|
||||
pure { fileName := c.fileName, fileMap := c.fileMap }
|
||||
|
||||
@[specialize] def runElab {α} (x : Elab α) : Frontend α :=
|
||||
do c ← getElabContext;
|
||||
monadLift $ EStateM.adaptState
|
||||
(fun (s : FrontendState) => (s.elabState, s.parserState))
|
||||
(fun es ps => { elabState := es, parserState := ps })
|
||||
(x c)
|
||||
|
||||
def elabCommandAtFrontend (stx : Syntax) : Frontend Unit :=
|
||||
runElab (elabCommand stx)
|
||||
|
||||
def updateCmdPos : Frontend Unit :=
|
||||
modify $ fun s => { elabState := { cmdPos := s.parserState.pos, .. s.elabState }, .. s }
|
||||
|
||||
def processCommand : Frontend Bool :=
|
||||
do updateCmdPos;
|
||||
s ← get;
|
||||
let es := s.elabState;
|
||||
let ps := s.parserState;
|
||||
c ← read;
|
||||
match Parser.parseCommand es.env c ps es.messages with
|
||||
| (cmd, ps, messages) => do
|
||||
set { elabState := { messages := messages, .. es }, parserState := ps };
|
||||
if Parser.isEOI cmd || Parser.isExitCommand cmd then do
|
||||
pure true -- Done
|
||||
else do
|
||||
catch (elabCommandAtFrontend cmd) $ fun e => runElab (logElabException e);
|
||||
pure false
|
||||
|
||||
partial def processCommandsAux : Unit → Frontend Unit
|
||||
| () => do
|
||||
done ← processCommand;
|
||||
if done then pure ()
|
||||
else processCommandsAux ()
|
||||
|
||||
def processCommands : Frontend Unit :=
|
||||
processCommandsAux ()
|
||||
|
||||
def testFrontend (input : String) (fileName : Option String := none) : IO (Environment × MessageLog) :=
|
||||
do env ← mkEmptyEnvironment;
|
||||
let fileName := fileName.getD "<input>";
|
||||
let ctx := Parser.mkParserContextCore env input fileName;
|
||||
match Parser.parseHeader env ctx with
|
||||
| (header, parserState, messages) => do
|
||||
(env, messages) ← processHeader header messages ctx;
|
||||
let elabState := { ElabState . env := env, messages := messages };
|
||||
match (processCommands ctx).run { elabState := elabState, parserState := parserState } with
|
||||
| EStateM.Result.ok _ s => pure (s.elabState.env, s.elabState.messages)
|
||||
| EStateM.Result.error _ s => pure (s.elabState.env, s.elabState.messages)
|
||||
|
||||
instance {α} : Inhabited (Elab α) :=
|
||||
⟨fun _ => arbitrary _⟩
|
||||
|
||||
def mkFreshName : Elab Name :=
|
||||
modifyGet $ fun s => (s.ngen.curr, { ngen := s.ngen.next, .. s })
|
||||
|
||||
def getScope : Elab ElabScope :=
|
||||
do s ← get; pure s.scopes.head!
|
||||
|
||||
def getOpenDecls : Elab (List OpenDecl) :=
|
||||
ElabScope.openDecls <$> getScope
|
||||
|
||||
def getUniverses : Elab (List Name) :=
|
||||
ElabScope.univs <$> getScope
|
||||
|
||||
def getNamespace : Elab Name :=
|
||||
do s ← get;
|
||||
match s.scopes with
|
||||
| [] => pure Name.anonymous
|
||||
| (sc::_) => pure sc.ns
|
||||
|
||||
@[specialize] def modifyScope (f : ElabScope → ElabScope) : Elab Unit :=
|
||||
modify $ fun s =>
|
||||
{ scopes := match s.scopes with
|
||||
| h::t => f h :: t
|
||||
| [] => [], -- unreachable
|
||||
.. s }
|
||||
|
||||
@[specialize] def modifyGetScope {α} [Inhabited α] (f : ElabScope → α × ElabScope) : Elab α :=
|
||||
modifyGet $ fun s =>
|
||||
match s with
|
||||
| { scopes := h::t, .. } =>
|
||||
let (a, h) := f h;
|
||||
(a, { scopes := h :: t, .. s })
|
||||
| _ => (arbitrary _, s)
|
||||
|
||||
def localContext : Elab LocalContext :=
|
||||
do scope ← getScope; pure scope.lctx
|
||||
|
||||
def mkLocalDecl (userName : Name) (type : Expr) (bi : BinderInfo := BinderInfo.default) : Elab Expr :=
|
||||
do idx ← mkFreshName;
|
||||
modifyScope $ fun scope => { lctx := scope.lctx.mkLocalDecl idx userName type bi, .. scope };
|
||||
pure (mkFVar idx)
|
||||
|
||||
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 :=
|
||||
do scope ← getScope;
|
||||
let n := anonymousInstNamePrefix.appendIndexAfter scope.nextInstIdx;
|
||||
modifyScope $ fun scope => { nextInstIdx := scope.nextInstIdx + 1, .. scope };
|
||||
pure n
|
||||
|
||||
def resolveNamespaceUsingScopes (env : Environment) (n : Name) : List ElabScope → Option Name
|
||||
| [] => none
|
||||
| { ns := ns, .. } :: scopes => if isNamespace env (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingScopes scopes
|
||||
|
||||
def resolveNamespaceUsingOpenDecls (env : Environment) (n : Name) : List OpenDecl → Option Name
|
||||
| [] => none
|
||||
| OpenDecl.simple ns [] :: ds => if isNamespace env (ns ++ n) then some (ns ++ n) else resolveNamespaceUsingOpenDecls ds
|
||||
| _ :: ds => resolveNamespaceUsingOpenDecls ds
|
||||
|
||||
/-
|
||||
Given a name `n` try to find namespace it refers to. The resolution procedure works as follows
|
||||
1- If `n` is the extact name of an existing namespace, then return `n`
|
||||
2- If `n` is in the scope of `namespace` commands declaring namespace headers `h_1`, ..., `h_n`,
|
||||
then return `h_1 ++ ... ++ h_i ++ n` if it is the name of an existing namespace. We search "backwards".
|
||||
3- Finally, for each command `open N`, return `N ++ n` if it is the name of an existing namespace.
|
||||
We search "backwards" again. That is, we try the most recent `open` command first.
|
||||
We only consider simple `open` commands.
|
||||
-/
|
||||
def resolveNamespace (n : Name) : Elab Name :=
|
||||
do s ← get;
|
||||
if isNamespace s.env n then pure n
|
||||
else match resolveNamespaceUsingScopes s.env n s.scopes with
|
||||
| some n => pure n
|
||||
| none => do
|
||||
openDecls ← getOpenDecls;
|
||||
match resolveNamespaceUsingOpenDecls s.env n openDecls with
|
||||
| some n => pure n
|
||||
| none => throw (ElabException.other ("unknown namespace '" ++ toString n ++ "'"))
|
||||
|
||||
@[inline] def withNewScope {α} (x : Elab α) : Elab α :=
|
||||
do modify $ fun s => { scopes := s.scopes.head! :: s.scopes, .. s };
|
||||
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)
|
||||
```
|
||||
and we would not need unsafe features for implementing `runIO`.
|
||||
We say `Elab` is "morally" built on top of `IO`. -/
|
||||
unsafe def runIOUnsafe {α : Type} (x : IO α) : Elab α :=
|
||||
match unsafeIO x with
|
||||
| Except.ok a => pure a
|
||||
| Except.error e => throw (ElabException.io e)
|
||||
|
||||
@[implementedBy runIOUnsafe]
|
||||
constant runIO {α : Type} (x : IO α) : Elab α := arbitrary _
|
||||
|
||||
end Elab
|
||||
-/
|
||||
end Elab
|
||||
end Lean
|
||||
1657
tmp/PreludeNew.lean
1657
tmp/PreludeNew.lean
File diff suppressed because it is too large
Load diff
|
|
@ -1,81 +0,0 @@
|
|||
import Init.Lean
|
||||
|
||||
open Lean
|
||||
|
||||
inductive Pattern
|
||||
| Inaccessible (e : Expr)
|
||||
| Var (fvarId : FVarId)
|
||||
| Ctor (fields : List Pattern)
|
||||
| Val (e : Expr)
|
||||
| ArrayLit (xs : List Pattern)
|
||||
|
||||
structure AltLHS :=
|
||||
(fvarIds : List FVarId) -- free variables used in the patterns
|
||||
(patterns : List Pattern) -- We use `List Pattern` since we have nary match-expressions.
|
||||
|
||||
abbrev AltToMinorsMap := PersistentHashMap Nat (List Nat)
|
||||
|
||||
structure ElimResult :=
|
||||
(numMinors : Nat) -- It is the number of alternatives (Reason: support for overlapping equations)
|
||||
(numEqs : Nat) -- It is the number of minors (Reason: users may want equations that hold definitionally)
|
||||
(elim : Expr) -- The eliminator. It is not just `Expr.const elimName` because the type of the major premises may contain free variables.
|
||||
(altMap : AltToMinorsMap) -- each alternative may be "expanded" into multiple minor premise
|
||||
|
||||
|
||||
/-
|
||||
Given a list of major premises `xs` and alternative left-hand-sides, generate an elimination
|
||||
principle with name `elimName` and equation lemmas for it.
|
||||
-/
|
||||
-- def mkElim (elimName : Name) (xs : List FVarId) (lhss : List AltLHS) : MetaM ElimResult :=
|
||||
-- sorry
|
||||
|
||||
universes u v
|
||||
|
||||
inductive Vec (α : Type u) : Nat → Type u
|
||||
| nil {} : Vec 0
|
||||
| cons : α → forall {n : Nat}, Vec n → Vec (n+1)
|
||||
|
||||
def Vec.elim {α : Type u} (C : forall (n : Nat), Vec α n → Vec α n → Sort v) {n : Nat} (v w : Vec α n)
|
||||
(h₁ : Unit → C 0 Vec.nil Vec.nil)
|
||||
(h₂ : forall (hdv : α) (n : Nat) (tlv : Vec α n) (hdw : α) (tlw : Vec α n), C (n+1) (Vec.cons hdv tlv) (Vec.cons hdw tlw))
|
||||
: C n v w :=
|
||||
match n, v, w with
|
||||
| .(0), Vec.nil, Vec.nil => h₁ ()
|
||||
| .(n+1), @Vec.cons .(α) hdv n tlv, @Vec.cons .(α) hdw .(n) tlw => h₂ hdv n tlv hdw tlw
|
||||
|
||||
def Vec.elimHEq {α : Type u} (C : forall (n : Nat) (v w : Vec α n), Sort v) {n : Nat} (v w : Vec α n)
|
||||
(h₁ : v ≅ @Vec.nil α → w ≅ @Vec.nil α → C 0 Vec.nil Vec.nil)
|
||||
(h₂ : forall (hdv : α) (n : Nat) (tlv : Vec α n) (hdw : α) (tlw : Vec α n), v ≅ Vec.cons hdv tlv → w ≅ Vec.cons hdw tlw → C (n+1) (Vec.cons hdv tlv) (Vec.cons hdw tlw))
|
||||
: C n v w :=
|
||||
Vec.elim (fun n' v' w' => v ≅ v' → w ≅ w' → C n' v' w') v w
|
||||
(fun _ => h₁)
|
||||
h₂
|
||||
(HEq.refl _)
|
||||
(HEq.refl _)
|
||||
|
||||
def Vec.elimEq {α : Type u} (C : forall (n : Nat) (v w : Vec α n), Sort v) {n : Nat} (v w : Vec α n)
|
||||
(h₁ : forall (h : n = 0), (Eq.rec v h : Vec α 0) = Vec.nil → (Eq.rec w h : Vec α 0) = Vec.nil → C 0 Vec.nil Vec.nil)
|
||||
(h₂ : forall (hdv : α) (n' : Nat) (tlv : Vec α n')
|
||||
(hdw : α) (tlw : Vec α n')
|
||||
(h : n = n' + 1),
|
||||
(Eq.rec v h : Vec α (n'+1)) = Vec.cons hdv tlv →
|
||||
(Eq.rec w h : Vec α (n'+1)) = Vec.cons hdw tlw →
|
||||
C (n'+1) (Vec.cons hdv tlv) (Vec.cons hdw tlw))
|
||||
: C n v w :=
|
||||
Vec.elim (fun n' v' w' => forall (h : n = n'), (Eq.rec v h : Vec α n') = v' → (Eq.rec w h : Vec α n') = w' → C n' v' w') v w
|
||||
(fun _ => h₁)
|
||||
h₂
|
||||
rfl
|
||||
rfl
|
||||
rfl
|
||||
|
||||
def List.elim {α : Type u} (C : List α → Sort v) (as : List α)
|
||||
(h₁ : Unit → C [])
|
||||
(h₂ : forall a, C [a])
|
||||
(h₃ : forall (a₁ : α) (as₁ : List α) (a₂ : α) (as₂ : List α), as₁ = a₂ :: as₂ → C (a₁::a₂::as₂))
|
||||
: C as :=
|
||||
List.casesOn as
|
||||
(h₁ ())
|
||||
(fun a r => @List.casesOn _ (fun as => r = as → C (a::as)) r
|
||||
(fun _ => h₂ a)
|
||||
(fun b bs h => h₃ a r b bs h) rfl)
|
||||
|
|
@ -1,140 +0,0 @@
|
|||
universes u v
|
||||
|
||||
inductive Foo (α : Type u)
|
||||
| leaf (a : α) : Foo
|
||||
| node (left : Foo) (right : Foo) : Foo
|
||||
| cons (head : α) (tail : Foo) : Foo
|
||||
|
||||
def Foo.elim {α : Type u} (C : Foo α → Foo α → Sort v) (x y : Foo α)
|
||||
(h₁ : forall (a₁ a₂ : α), C (Foo.leaf a₁) (Foo.leaf a₂))
|
||||
(h₂ : forall (l₁ r₁ l₂ r₂ : Foo α), C (Foo.node l₁ r₁) (Foo.node l₂ r₂))
|
||||
(h₃ : forall (h₁ t₁ h₂ t₂), C (Foo.cons h₁ t₁) (Foo.cons h₂ t₂))
|
||||
(h₄ : forall (x y), C x y)
|
||||
: C x y :=
|
||||
Foo.casesOn x
|
||||
(fun a₁ => Foo.casesOn y
|
||||
(fun a₂ => h₁ a₁ a₂)
|
||||
(fun l₂ r₂ => h₄ (Foo.leaf a₁) (Foo.node l₂ r₂))
|
||||
(fun h₂ t₂ => h₄ (Foo.leaf a₁) (Foo.cons h₂ t₂)))
|
||||
(fun l₁ r₁ => Foo.casesOn y
|
||||
(fun a₂ => h₄ (Foo.node l₁ r₁) (Foo.leaf a₂))
|
||||
(fun l₂ r₂ => h₂ l₁ r₁ l₂ r₂)
|
||||
(fun h₂ t₂ => h₄ (Foo.node l₁ r₁) (Foo.cons h₂ t₂)))
|
||||
(fun h₁ t₁ => Foo.casesOn y
|
||||
(fun a₂ => h₄ (Foo.cons h₁ t₁) (Foo.leaf a₂))
|
||||
(fun l₂ r₂ => h₄ (Foo.cons h₁ t₁) (Foo.node l₂ r₂))
|
||||
(fun h₂ t₂ => h₃ h₁ t₁ h₂ t₂))
|
||||
|
||||
def f : List Nat → List Nat → List Nat
|
||||
| x::xs, _ => []
|
||||
| _, [] => []
|
||||
| xs, ys => xs ++ ys
|
||||
|
||||
def List.elim (C : List Nat → List Nat → Sort v) (xs ys : List Nat)
|
||||
(h₁ : forall x xs ys, C (x::xs) ys)
|
||||
(h₂ : forall xs, C xs [])
|
||||
(h₃ : forall xs ys, C xs ys)
|
||||
: C xs ys :=
|
||||
List.casesOn xs
|
||||
(List.casesOn ys
|
||||
(h₂ [])
|
||||
(fun y ys => h₃ [] (y::ys)))
|
||||
(fun x xs => h₁ x xs ys)
|
||||
|
||||
theorem List.elim.eq1 (C : List Nat → List Nat → Sort v)
|
||||
(h₁ : forall x xs ys, C (x::xs) ys)
|
||||
(h₂ : forall xs, C xs [])
|
||||
(h₃ : forall xs ys, C xs ys)
|
||||
(x : Nat) (xs ys : List Nat)
|
||||
: List.elim C (x::xs) ys h₁ h₂ h₃ = h₁ x xs ys :=
|
||||
rfl
|
||||
|
||||
theorem List.elim.eq2 (C : List Nat → List Nat → Sort v)
|
||||
(h₁ : forall x xs ys, C (x::xs) ys)
|
||||
(h₂ : forall xs, C xs [])
|
||||
(h₃ : forall xs ys, C xs ys)
|
||||
(xs : List Nat)
|
||||
: (forall x' xs', xs = x'::xs' → False) → List.elim C xs [] h₁ h₂ h₃ = h₂ xs :=
|
||||
List.casesOn xs
|
||||
(fun _ => rfl)
|
||||
(fun x xs h => False.elim (h x xs rfl))
|
||||
|
||||
theorem List.elim.eq3 (C : List Nat → List Nat → Sort v)
|
||||
(h₁ : forall x xs ys, C (x::xs) ys)
|
||||
(h₂ : forall xs, C xs [])
|
||||
(h₃ : forall xs ys, C xs ys)
|
||||
(xs : List Nat) (ys : List Nat)
|
||||
: (forall x' xs', xs = x'::xs' → False) → (ys = [] → False) → List.elim C xs ys h₁ h₂ h₃ = h₃ xs ys :=
|
||||
List.casesOn xs
|
||||
(List.casesOn ys
|
||||
(fun _ h => False.elim (h rfl))
|
||||
(fun y ys _ _ => rfl))
|
||||
(fun x xs h _ => False.elim (h x xs rfl))
|
||||
|
||||
theorem List.elim.eq3.a (C : List Nat → List Nat → Sort v)
|
||||
(h₁ : forall x xs ys, C (x::xs) ys)
|
||||
(h₂ : forall xs, C xs [])
|
||||
(h₃ : forall xs ys, C xs ys)
|
||||
(y : Nat) (ys : List Nat)
|
||||
: List.elim C [] (y::ys) h₁ h₂ h₃ = h₃ [] (y::ys) :=
|
||||
rfl
|
||||
|
||||
def List.elim2 (C : List Nat → List Nat → Sort v) (xs ys : List Nat)
|
||||
(h₁ : forall x xs ys, C (x::xs) ys)
|
||||
(h₂ : forall xs, (forall (x' : Nat) (xs' : List Nat), xs = x' :: xs' → False) → C xs [])
|
||||
(h₃ : forall xs ys, (forall (x' : Nat) (xs' : List Nat), xs = x' :: xs' → False) → (ys = [] → False) → C xs ys)
|
||||
: C xs ys :=
|
||||
List.casesOn xs
|
||||
(List.casesOn ys
|
||||
(h₂ [] (fun _ _ h => List.noConfusion h))
|
||||
(fun y ys => h₃ [] (y::ys) (fun _ _ h => List.noConfusion h) (fun h => List.noConfusion h)))
|
||||
(fun x xs => h₁ x xs ys)
|
||||
|
||||
def List.elim3 (C : List Nat → List Nat → List Nat → Sort v) (xs ys zs : List Nat)
|
||||
(h₁ : forall zs, C [] [] zs)
|
||||
(h₂ : forall xs ys, C xs ys [])
|
||||
(h₃ : forall xs ys zs, C xs ys zs)
|
||||
: C xs ys zs :=
|
||||
List.casesOn xs
|
||||
(List.casesOn ys
|
||||
(h₁ zs)
|
||||
(fun y ys => List.casesOn zs
|
||||
(h₃ [] (y::ys) [])
|
||||
(fun z zs => h₃ [] (y::ys) (z::zs))))
|
||||
(fun x xs =>
|
||||
(List.casesOn zs
|
||||
(h₂ (x::xs) ys)
|
||||
(fun z zs => h₃ (x::xs) ys (z::zs))))
|
||||
|
||||
theorem List.elim3.eq (C : List Nat → List Nat → List Nat → Sort v)
|
||||
(h₁ : forall zs, C [] [] zs)
|
||||
(h₂ : forall xs ys, C xs ys [])
|
||||
(h₃ : forall xs ys zs, C xs ys zs)
|
||||
(xs ys zs : List Nat)
|
||||
: (xs = [] → ys = [] → False) → (zs = [] → False) → List.elim3 C xs ys zs h₁ h₂ h₃ = h₃ xs ys zs :=
|
||||
List.casesOn xs
|
||||
(List.casesOn ys
|
||||
(fun h _ => False.elim (h rfl rfl))
|
||||
(fun y ys => List.casesOn zs
|
||||
(fun _ h => False.elim (h rfl))
|
||||
(fun z zs _ _ => rfl)))
|
||||
(fun x xs =>
|
||||
List.casesOn zs
|
||||
(fun _ h => False.elim (h rfl))
|
||||
(fun z zs _ _ => rfl))
|
||||
|
||||
theorem List.elim3.eq.a (C : List Nat → List Nat → List Nat → Sort v)
|
||||
(h₁ : forall zs, C [] [] zs)
|
||||
(h₂ : forall xs ys, C xs ys [])
|
||||
(h₃ : forall xs ys zs, C xs ys zs)
|
||||
(y : Nat) (ys : List Nat) (z : Nat) (zs : List Nat)
|
||||
: List.elim3 C [] (y::ys) (z::zs) h₁ h₂ h₃ = h₃ [] (y::ys) (z::zs) :=
|
||||
rfl
|
||||
|
||||
theorem List.elim3.eq.b (C : List Nat → List Nat → List Nat → Sort v)
|
||||
(h₁ : forall zs, C [] [] zs)
|
||||
(h₂ : forall xs ys, C xs ys [])
|
||||
(h₃ : forall xs ys zs, C xs ys zs)
|
||||
(x : Nat) (xs : List Nat) (y : Nat) (ys : List Nat) (z : Nat) (zs : List Nat)
|
||||
: List.elim3 C (x::xs) (y::ys) (z::zs) h₁ h₂ h₃ = h₃ (x::xs) (y::ys) (z::zs) :=
|
||||
rfl
|
||||
|
|
@ -1,193 +0,0 @@
|
|||
universes u v
|
||||
|
||||
namespace Experiment1
|
||||
inductive ArrayLitMatch (α : Type u)
|
||||
| sz0 {} : ArrayLitMatch
|
||||
| sz1 (a₁ : α) : ArrayLitMatch
|
||||
| sz2 (a₁ a₂ : α) : ArrayLitMatch
|
||||
| sz3 (a₁ a₂ a₃ : α) : ArrayLitMatch
|
||||
| other {} : ArrayLitMatch
|
||||
|
||||
def matchArrayLit {α : Type u} (a : Array α) : ArrayLitMatch α :=
|
||||
if a.size = 0 then
|
||||
ArrayLitMatch.sz0
|
||||
else if h : a.size = 1 then
|
||||
ArrayLitMatch.sz1 (a.getLit 0 h (ofDecideEqTrue rfl))
|
||||
else if h : a.size = 2 then
|
||||
ArrayLitMatch.sz2 (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl))
|
||||
else if h : a.size = 3 then
|
||||
ArrayLitMatch.sz3 (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))
|
||||
else
|
||||
ArrayLitMatch.other
|
||||
|
||||
def matchArrayLit.eq0 {α : Type u} : matchArrayLit (#[] : Array α) = ArrayLitMatch.sz0 :=
|
||||
rfl
|
||||
|
||||
def matchArrayLit.eq1 {α : Type u} (a₁ : α) : matchArrayLit #[a₁] = ArrayLitMatch.sz1 a₁ :=
|
||||
rfl
|
||||
|
||||
def matchArrayLit.eq2 {α : Type u} (a₁ a₂ : α) : matchArrayLit #[a₁, a₂] = ArrayLitMatch.sz2 a₁ a₂ :=
|
||||
rfl
|
||||
|
||||
def matchArrayLit.eq3 {α : Type u} (a₁ a₂ a₃ : α) : matchArrayLit #[a₁, a₂, a₃] = ArrayLitMatch.sz3 a₁ a₂ a₃ :=
|
||||
rfl
|
||||
|
||||
def matchArrayLit.eq4 {α : Type u} (a₁ a₂ a₃ a₄ : α) : matchArrayLit #[a₁, a₂, a₃, a₄] = ArrayLitMatch.other :=
|
||||
rfl
|
||||
end Experiment1
|
||||
|
||||
def toListLitAux {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
|
||||
| 0, hi, acc => acc
|
||||
| (i+1), hi, acc => toListLitAux i (Nat.leOfSuccLe hi) (a.getLit i hsz (Nat.ltOfLtOfEq (Nat.ltOfLtOfLe (Nat.ltSuccSelf i) hi) hsz) :: acc)
|
||||
|
||||
def toArrayLit {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
|
||||
List.toArray $ toListLitAux a n hsz n (hsz ▸ Nat.leRefl _) []
|
||||
|
||||
theorem toArrayLitEq {α : Type u} (a : Array α) (n : Nat) (hsz : a.size = n) : a = toArrayLit a n hsz :=
|
||||
-- TODO: this is painful to prove without proper automation
|
||||
sorry
|
||||
/-
|
||||
First, we need to prove
|
||||
∀ i j acc, i ≤ a.size → (toListLitAux a n hsz (i+1) hi acc).index j = if j < i then a.getLit j hsz _ else acc.index (j - i)
|
||||
by induction
|
||||
|
||||
Base case is trivial
|
||||
(j : Nat) (acc : List α) (hi : 0 ≤ a.size)
|
||||
|- (toListLitAux a n hsz 0 hi acc).index j = if j < 0 then a.getLit j hsz _ else acc.index (j - 0)
|
||||
... |- acc.index j = acc.index j
|
||||
|
||||
Induction
|
||||
|
||||
(j : Nat) (acc : List α) (hi : i+1 ≤ a.size)
|
||||
|- (toListLitAux a n hsz (i+1) hi acc).index j = if j < i + 1 then a.getLit j hsz _ else acc.index (j - (i + 1))
|
||||
... |- (toListLitAux a n hsz i hi' (a.getLit i hsz _ :: acc)).index j = if j < i + 1 then a.getLit j hsz _ else acc.index (j - (i + 1)) * by def
|
||||
... |- if j < i then a.getLit j hsz _ else (a.getLit i hsz _ :: acc).index (j-i) * by induction hypothesis
|
||||
=
|
||||
if j < i + 1 then a.getLit j hsz _ else acc.index (j - (i + 1))
|
||||
If j < i, then both are a.getLit j hsz _
|
||||
If j = i, then lhs reduces else-branch to (a.getLit i hsz _) and rhs is then-brachn (a.getLit i hsz _)
|
||||
If j >= i + 1, we use
|
||||
- j - i >= 1 > 0
|
||||
- (a::as).index k = as.index (k-1) If k > 0
|
||||
- j - (i + 1) = (j - i) - 1
|
||||
Then lhs = (a.getLit i hsz _ :: acc).index (j-i) = acc.index (j-i-1) = acc.index (j-(i+1)) = rhs
|
||||
|
||||
With this proof, we have
|
||||
|
||||
∀ j, j < n → (toListLitAux a n hsz n _ []).index j = a.getLit j hsz _
|
||||
|
||||
We also need
|
||||
|
||||
- (toListLitAux a n hsz n _ []).length = n
|
||||
- j < n -> (List.toArray as).getLit j _ _ = as.index j
|
||||
|
||||
Then using Array.extLit, we have that a = List.toArray $ toListLitAux a n hsz n _ []
|
||||
-/
|
||||
|
||||
theorem Array.eqLitOfSize0 {α : Type u} (a : Array α) (hsz : a.size = 0) : a = #[] :=
|
||||
toArrayLitEq a 0 hsz
|
||||
/-
|
||||
Array.ext a #[] h (fun i h₁ h₂ => absurd h₂ (Nat.notLtZero _))
|
||||
-/
|
||||
|
||||
theorem Array.eqLitOfSize1 {α : Type u} (a : Array α) (hsz : a.size = 1) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl)] :=
|
||||
toArrayLitEq a 1 hsz
|
||||
/-
|
||||
Array.extLit a #[a.getLit 0 hsz (ofDecideEqTrue rfl)] hsz rfl $ fun i =>
|
||||
match i with
|
||||
| 0 => fun hi => rfl
|
||||
| (n+1) => fun hi =>
|
||||
have n < 0 from hi;
|
||||
absurd this (Nat.notLtZero _)
|
||||
-/
|
||||
|
||||
theorem Array.eqLitOfSize2 {α : Type u} (a : Array α) (hsz : a.size = 2) : a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl)] :=
|
||||
toArrayLitEq a 2 hsz
|
||||
/-
|
||||
Array.extLit a #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl)] hsz rfl $ fun i =>
|
||||
match i with
|
||||
| 0 => fun hi => rfl
|
||||
| 1 => fun hi => rfl
|
||||
| (n+2) => fun hi =>
|
||||
have n < 0 from hi;
|
||||
absurd this (Nat.notLtZero _)
|
||||
-/
|
||||
|
||||
theorem Array.eqLitOfSize3 {α : Type u} (a : Array α) (hsz : a.size = 3) :
|
||||
a = #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl), a.getLit 2 hsz (ofDecideEqTrue rfl)] :=
|
||||
toArrayLitEq a 3 hsz
|
||||
/-
|
||||
Array.extLit a #[a.getLit 0 hsz (ofDecideEqTrue rfl), a.getLit 1 hsz (ofDecideEqTrue rfl), a.getLit 2 hsz (ofDecideEqTrue rfl)] hsz rfl $ fun i =>
|
||||
match i with
|
||||
| 0 => fun hi => rfl
|
||||
| 1 => fun hi => rfl
|
||||
| 2 => fun hi => rfl
|
||||
| (n+3) => fun hi =>
|
||||
have n < 0 from hi;
|
||||
absurd this (Nat.notLtZero _)
|
||||
-/
|
||||
|
||||
/-
|
||||
Matcher for the following patterns
|
||||
```
|
||||
| #[] => _
|
||||
| #[a₁] => _
|
||||
| #[a₁, a₂, a₃] => _
|
||||
| a => _
|
||||
``` -/
|
||||
def matchArrayLit {α : Type u} (C : Array α → Sort v) (a : Array α)
|
||||
(h₁ : Unit → C #[])
|
||||
(h₂ : ∀ a₁, C #[a₁])
|
||||
(h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃])
|
||||
(h₄ : ∀ a, C a)
|
||||
: C a :=
|
||||
if h : a.size = 0 then
|
||||
@Eq.rec _ _ (fun x _ => C x) (h₁ ()) _ (toArrayLitEq a 0 h).symm
|
||||
else if h : a.size = 1 then
|
||||
@Eq.rec _ _ (fun x _ => C x) (h₂ (a.getLit 0 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 1 h).symm
|
||||
else if h : a.size = 3 then
|
||||
@Eq.rec _ _ (fun x _ => C x) (h₃ (a.getLit 0 h (ofDecideEqTrue rfl)) (a.getLit 1 h (ofDecideEqTrue rfl)) (a.getLit 2 h (ofDecideEqTrue rfl))) _ (toArrayLitEq a 3 h).symm
|
||||
else
|
||||
h₄ a
|
||||
|
||||
/- Equational lemmas that should be generated automatically. -/
|
||||
theorem matchArrayLit.eq1 {α : Type u} (C : Array α → Sort v)
|
||||
(h₁ : Unit → C #[])
|
||||
(h₂ : ∀ a₁, C #[a₁])
|
||||
(h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃])
|
||||
(h₄ : ∀ a, C a)
|
||||
: matchArrayLit C #[] h₁ h₂ h₃ h₄ = h₁ () :=
|
||||
rfl
|
||||
|
||||
theorem matchArrayLit.eq2 {α : Type u} (C : Array α → Sort v)
|
||||
(h₁ : Unit → C #[])
|
||||
(h₂ : ∀ a₁, C #[a₁])
|
||||
(h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃])
|
||||
(h₄ : ∀ a, C a)
|
||||
(a₁ : α)
|
||||
: matchArrayLit C #[a₁] h₁ h₂ h₃ h₄ = h₂ a₁ :=
|
||||
rfl
|
||||
|
||||
theorem matchArrayLit.eq3 {α : Type u} (C : Array α → Sort v)
|
||||
(h₁ : Unit → C #[])
|
||||
(h₂ : ∀ a₁, C #[a₁])
|
||||
(h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃])
|
||||
(h₄ : ∀ a, C a)
|
||||
(a₁ a₂ a₃ : α)
|
||||
: matchArrayLit C #[a₁, a₂, a₃] h₁ h₂ h₃ h₄ = h₃ a₁ a₂ a₃ :=
|
||||
rfl
|
||||
|
||||
theorem matchArrayLit.eq4 {α : Type u} (C : Array α → Sort v)
|
||||
(h₁ : Unit → C #[])
|
||||
(h₂ : ∀ a₁, C #[a₁])
|
||||
(h₃ : ∀ a₁ a₂ a₃, C #[a₁, a₂, a₃])
|
||||
(h₄ : ∀ a, C a)
|
||||
(a : Array α)
|
||||
(n₁ : a.size ≠ 0) (n₂ : a.size ≠ 1) (n₃ : a.size ≠ 3)
|
||||
: matchArrayLit C a h₁ h₂ h₃ h₄ = h₄ a :=
|
||||
match a, n₁, n₂, n₃ with
|
||||
| ⟨0, _⟩, n₁, _, _ => absurd rfl n₁
|
||||
| ⟨1, _⟩, _, n₂, _ => absurd rfl n₂
|
||||
| ⟨2, _⟩, _, _, _ => rfl
|
||||
| ⟨3, _⟩, _, _, n₃ => absurd rfl n₃
|
||||
| ⟨n+4, _⟩, _, _, _ => rfl
|
||||
|
|
@ -1,46 +0,0 @@
|
|||
universes v
|
||||
/-
|
||||
matcher for the following patterns
|
||||
```
|
||||
| "hello" => _
|
||||
| "world" => _
|
||||
| a => _
|
||||
``` -/
|
||||
def matchString (C : String → Sort v) (s : String)
|
||||
(h₁ : Unit → C "hello")
|
||||
(h₂ : Unit → C "world")
|
||||
(h₃ : ∀ s, C s)
|
||||
: C s :=
|
||||
dite (s = "hello")
|
||||
(fun h => @Eq.ndrec _ _ (fun x => C x) (h₁ ()) _ h.symm)
|
||||
(fun _ => dite (s = "world")
|
||||
(fun h => @Eq.ndrec _ _ (fun x => C x) (h₂ ()) _ h.symm)
|
||||
(fun _ => h₃ s))
|
||||
|
||||
theorem matchString.Eq1 (C : String → Sort v)
|
||||
(h₁ : Unit → C "hello")
|
||||
(h₂ : Unit → C "world")
|
||||
(h₃ : ∀ s, C s)
|
||||
: matchString C "hello" h₁ h₂ h₃ = h₁ () :=
|
||||
difPos rfl
|
||||
|
||||
axiom neg1 : "world" ≠ "hello"
|
||||
|
||||
theorem matchString.Eq2 (C : String → Sort v)
|
||||
(h₁ : Unit → C "hello")
|
||||
(h₂ : Unit → C "world")
|
||||
(h₃ : ∀ s, C s)
|
||||
: matchString C "world" h₁ h₂ h₃ = h₂ () :=
|
||||
have aux₁ : matchString C "world" h₁ h₂ h₃ = if h : "world" = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ "world" from difNeg neg1;
|
||||
have aux₂ : (if h : "world" = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ "world" : C "world") = h₂ () from difPos rfl;
|
||||
Eq.trans aux₁ aux₂
|
||||
|
||||
theorem matchString.Eq3 (C : String → Sort v)
|
||||
(h₁ : Unit → C "hello")
|
||||
(h₂ : Unit → C "world")
|
||||
(h₃ : ∀ s, C s)
|
||||
(s : String) (n₁ : s ≠ "hello") (n₂ : s ≠ "world")
|
||||
: matchString C s h₁ h₂ h₃ = h₃ s :=
|
||||
have aux₁ : matchString C s h₁ h₂ h₃ = if h : s = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ s from difNeg n₁;
|
||||
have aux₂ : (if h : s = "world" then @Eq.rec _ _ (fun x _ => C x) (h₂ ()) _ h.symm else h₃ s : C s) = h₃ s from difNeg n₂;
|
||||
Eq.trans aux₁ aux₂
|
||||
File diff suppressed because it is too large
Load diff
|
|
@ -1,544 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Macro Expander for the Lean language, using a variant of the [sets of scopes](http://www.cs.utah.edu/plt/Scope-sets/) hygiene algorithm.
|
||||
|
||||
TODO(Sebastian): document/link to documentation of algorithm
|
||||
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.module
|
||||
import init.lean.expr
|
||||
|
||||
namespace Lean
|
||||
namespace Expander
|
||||
open Parser
|
||||
open Parser.Combinators
|
||||
open Parser.Term
|
||||
open Parser.command
|
||||
|
||||
structure TransformerConfig extends FrontendConfig
|
||||
-- TODO(Sebastian): the recursion point for `localExpand` probably needs to be stored here
|
||||
|
||||
instance transformerConfigCoeFrontendConfig : HasCoe TransformerConfig FrontendConfig :=
|
||||
⟨TransformerConfig.toFrontendConfig⟩
|
||||
|
||||
-- TODO(Sebastian): recursive expansion
|
||||
@[derive Monad MonadReader MonadExcept]
|
||||
def TransformM := ReaderT FrontendConfig $ ExceptT Message Id
|
||||
abbrev transformer := Syntax → TransformM (Option Syntax)
|
||||
|
||||
/-- We allow macros to refuse expansion. This means that nodes can decide whether to act as macros
|
||||
or not depending on their contents, allowing them to unfold to some normal form without changing
|
||||
the general Node kind and shape (and thus View Type). -/
|
||||
def noExpansion : TransformM (Option Syntax) :=
|
||||
pure none
|
||||
|
||||
def error {m : Type → Type} {ρ : Type} [Monad m] [MonadReader ρ m] [HasLiftT ρ FrontendConfig]
|
||||
[MonadExcept Message m] {α : Type}
|
||||
(context : Option Syntax) (text : String) : m α :=
|
||||
do cfg ← read,
|
||||
throw {
|
||||
filename := FrontendConfig.filename ↑cfg,
|
||||
pos := (FrontendConfig.fileMap ↑cfg).toPosition $ (context >>= Syntax.getPos).getOrElse (default _),
|
||||
text := text
|
||||
}
|
||||
|
||||
/-- Coercion useful for introducing macro-local variables. Use `globId` to refer to global bindings instead. -/
|
||||
instance coeNameIdent : HasCoe Name SyntaxIdent :=
|
||||
⟨λ n, {val := n, rawVal := Substring.ofString n.toString}⟩
|
||||
|
||||
/-- Create an identifier preresolved against a global binding. Because we cannot use Syntax quotations yet,
|
||||
which the Expander would have preresolved against the global context at macro declaration time,
|
||||
we have to do the preresolution manually instead. -/
|
||||
def globId (n : Name) : Syntax :=
|
||||
review identUnivs {
|
||||
id :={val := n, rawVal := Substring.ofString n.toString, preresolved := [n]},
|
||||
}
|
||||
|
||||
instance coeIdentIdentUnivs : HasCoe SyntaxIdent identUnivs.View :=
|
||||
⟨λ id, {id := id}⟩
|
||||
|
||||
instance coeIdentBinderId : HasCoe SyntaxIdent binderIdent.View :=
|
||||
⟨binderIdent.View.id⟩
|
||||
|
||||
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⟩
|
||||
|
||||
instance coeSimpleBinderBinders : HasCoe Term.simpleBinder.View Term.binders.View :=
|
||||
⟨Term.binders.View.simple⟩
|
||||
|
||||
instance coeBinderBracketedBinder : HasCoe Term.binder.View Term.bracketedBinder.View :=
|
||||
⟨λ b, match b with
|
||||
| binder.View.bracketed bb := bb
|
||||
| binder.View.unbracketed bc := Term.bracketedBinder.View.explicit
|
||||
{content := explicitBinderContent.View.other bc}⟩
|
||||
|
||||
section «notation»
|
||||
open Parser.command.NotationSpec
|
||||
|
||||
/-- A notation together with a unique Node kind. -/
|
||||
structure NotationMacro :=
|
||||
(kind : SyntaxNodeKind)
|
||||
(nota : notation.View)
|
||||
|
||||
/-- Helper State of the loop in `mkNotationTransformer`. -/
|
||||
structure NotationTransformerState :=
|
||||
(stx : Syntax)
|
||||
-- children of `stx` that have not been consumed yet
|
||||
(stxArgs : List Syntax := [])
|
||||
-- substitutions for notation variables (reversed)
|
||||
(substs : List (SyntaxIdent × Syntax) := [])
|
||||
-- filled by `binders` transitions, consumed by `scoped` actions
|
||||
(scoped : Option $ Term.binders.View := none)
|
||||
|
||||
private def popStxArg : StateT NotationTransformerState TransformM Syntax :=
|
||||
do st ← get,
|
||||
match st.stxArgs with
|
||||
| Arg::args := set {st with stxArgs := args} *> pure Arg
|
||||
| _ := error st.stx "mkNotationTransformer: unreachable"
|
||||
|
||||
def mkNotationTransformer (nota : NotationMacro) : transformer :=
|
||||
λ stx, do
|
||||
some {args := stxArgs, ..} ← pure stx.asNode
|
||||
| error stx "mkNotationTransformer: unreachable",
|
||||
flip StateT.run' {NotationTransformerState . stx := stx, stxArgs := stxArgs} $ do
|
||||
let spec := nota.nota.spec,
|
||||
-- Walk through the notation specification, consuming `stx` args and building up substitutions
|
||||
-- for the notation RHS.
|
||||
-- Also see `CommandParserConfig.registerNotationParser` for the expected structure of `stx`.
|
||||
match spec.prefixArg with
|
||||
| none := pure ()
|
||||
| some Arg := do { stxArg ← popStxArg, modify $ λ st, {st with substs := (Arg, stxArg)::st.substs} },
|
||||
nota.nota.spec.rules.mfor (λ r : rule.View, do
|
||||
match r.symbol with
|
||||
| notationSymbol.View.quoted {symbol := some a ..} := popStxArg
|
||||
| _ := error stx "mkNotationTransformer: unreachable",
|
||||
match r.transition with
|
||||
| some (transition.View.binder b) :=
|
||||
do { stxArg ← popStxArg, modify $ λ st, {st with scoped := some $ binders.View.extended {leadingIds := [view binderIdent.Parser stxArg]}} }
|
||||
| some (transition.View.binders b) :=
|
||||
do { stxArg ← popStxArg, modify $ λ st, {st with scoped := some $ view Term.binders.Parser stxArg} }
|
||||
| some (transition.View.Arg {action := none, id := id}) :=
|
||||
do { stxArg ← popStxArg, modify $ λ st, {st with substs := (id, stxArg)::st.substs} }
|
||||
| some (transition.View.Arg {action := some {kind := actionKind.View.prec _}, id := id}) :=
|
||||
do { stxArg ← popStxArg, modify $ λ st, {st with substs := (id, stxArg)::st.substs} }
|
||||
| some (transition.View.Arg {action := some {kind := actionKind.View.scoped sc}, id := id}) := do
|
||||
stxArg ← popStxArg,
|
||||
{scoped := some bnders, ..} ← get
|
||||
| error stx "mkNotationTransformer: unreachable",
|
||||
-- TODO(Sebastian): not correct with multiple binders
|
||||
let scLam := review lambda {binders := [sc.id], body := sc.Term},
|
||||
let lam := review lambda {binders := bnders, body := stxArg},
|
||||
let Arg := review app {fn := scLam, Arg := lam},
|
||||
modify $ λ st, {st with substs := (id, Arg)::st.substs}
|
||||
| none := pure ()
|
||||
| _ := error stx "mkNotationTransformer: unimplemented"),
|
||||
st ← get,
|
||||
-- apply substitutions
|
||||
-- HACK: this substitution completely disregards binders on the notation's RHS.
|
||||
-- We have discussed switching to a more explicit antiquotation Syntax like %%_
|
||||
-- that cannot be abstracted over.
|
||||
let substs := st.substs.map (λ ⟨id, t⟩, (id.val, t)),
|
||||
let t := nota.nota.Term.replace $ λ stx, match tryView identUnivs stx with
|
||||
| some {id := id, univs := none} := pure $ substs.lookup id.val
|
||||
| _ := pure none,
|
||||
pure $ some $ t
|
||||
|
||||
def mixfixToNotationSpec (k : mixfix.kind.View) (sym : notationSymbol.View) : TransformM NotationSpec.View :=
|
||||
let prec := match sym with
|
||||
| notationSymbol.View.quoted q := q.prec
|
||||
/-| _ := none -/ in
|
||||
-- `notation` allows more Syntax after `:` than mixfix commands, so we have to do a small conversion
|
||||
let precToAction := λ prec, {action.View . kind := actionKind.View.prec prec} in
|
||||
match k with
|
||||
| mixfix.kind.View.prefix _ :=
|
||||
-- `prefix sym:prec` ~> `notation sym:prec b:prec`
|
||||
pure {
|
||||
rules := [{
|
||||
symbol := sym,
|
||||
transition := transition.View.Arg {id := `b,
|
||||
action := precToAction <$> precedence.View.Term <$> prec}}]}
|
||||
| mixfix.kind.View.postfix _ :=
|
||||
-- `postfix tk:prec` ~> `notation a tk:prec`
|
||||
pure {
|
||||
prefixArg := `a,
|
||||
rules := [{symbol := sym}]}
|
||||
| mixfix.kind.View.infixr _ := do
|
||||
-- `infixr tk:prec` ~> `notation a tk:prec b:(prec-1)`
|
||||
act ← match prec with
|
||||
| some prec := if prec.Term.toNat = 0
|
||||
then error (review «precedence» prec) "invalid `infixr` declaration, given precedence must greater than zero"
|
||||
else pure $ some $ precToAction $ precedenceTerm.View.lit $ precedenceLit.View.num $ number.View.ofNat $ prec.Term.toNat - 1
|
||||
| none := pure none,
|
||||
pure {
|
||||
prefixArg := `a,
|
||||
rules := [{
|
||||
symbol := sym,
|
||||
transition := transition.View.Arg {id := `b,
|
||||
action := act}}]}
|
||||
| _ :=
|
||||
-- `infix/infixl tk:prec` ~> `notation a tk:prec b:prec`
|
||||
pure {
|
||||
prefixArg := `a,
|
||||
rules := [{
|
||||
symbol := sym,
|
||||
transition := transition.View.Arg {id := `b,
|
||||
action := precToAction <$> precedence.View.Term <$> prec}}]}
|
||||
|
||||
def mixfix.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view mixfix stx,
|
||||
let notaSym := match v.symbol with
|
||||
| mixfixSymbol.View.quoted q := notationSymbol.View.quoted q
|
||||
| mixfixSymbol.View.unquoted u := notationSymbol.View.quoted {symbol := u},
|
||||
spec ← mixfixToNotationSpec v.kind notaSym,
|
||||
let Term := match v.kind with
|
||||
| mixfix.kind.View.prefix _ :=
|
||||
-- `prefix tk:prec? := e` ~> `notation tk:prec? b:prec? := e b`
|
||||
review app {fn := v.Term, Arg := review identUnivs `b}
|
||||
| mixfix.kind.View.postfix _ :=
|
||||
-- `postfix tk:prec? := e` ~> `notation tk:prec? b:prec? := e b`
|
||||
review app {fn := v.Term, Arg := review identUnivs `a}
|
||||
| _ :=
|
||||
review app {fn := review app {fn := v.Term, Arg := review identUnivs `a}, Arg := review identUnivs `b},
|
||||
pure $ review «notation» {«local» := v.local, spec := spec, Term := Term}
|
||||
|
||||
def reserveMixfix.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view reserveMixfix stx,
|
||||
spec ← mixfixToNotationSpec v.kind v.symbol,
|
||||
pure $ review reserveNotation {spec := spec}
|
||||
|
||||
end «notation»
|
||||
|
||||
def mkSimpleBinder (id : SyntaxIdent) (bi : BinderInfo) (type : Syntax) : simpleBinder.View :=
|
||||
let bc : binderContent.View := {ids := [id], type := some {type := type}} in
|
||||
match bi with
|
||||
| BinderInfo.default := simpleBinder.View.explicit {id := id, type := type}
|
||||
| BinderInfo.implicit := simpleBinder.View.implicit {id := id, type := type}
|
||||
| BinderInfo.strictImplicit := simpleBinder.View.strictImplicit {id := id, type := type}
|
||||
| BinderInfo.instImplicit := simpleBinder.View.instImplicit {id := id, type := type}
|
||||
| BinderInfo.auxDecl := /- should not happen -/
|
||||
simpleBinder.View.explicit {id := id, type := type}
|
||||
|
||||
def binderIdentToIdent : binderIdent.View → SyntaxIdent
|
||||
| (binderIdent.View.id id) := id
|
||||
| (binderIdent.View.hole _) := "a"
|
||||
|
||||
def getOptType : Option typeSpec.View → Syntax
|
||||
| none := review hole {}
|
||||
| (some v) := v.type
|
||||
|
||||
def expandBracketedBinder : bracketedBinder.View → TransformM (List simpleBinder.View)
|
||||
-- local notation: should have been handled by caller, erase
|
||||
| (bracketedBinder.View.explicit {content := explicitBinderContent.View.notation _}) := pure []
|
||||
| mbb := do
|
||||
(bi, bc) ← match mbb with
|
||||
| bracketedBinder.View.explicit {content := bc} := pure (match bc with
|
||||
| explicitBinderContent.View.other bc := (BinderInfo.default, bc)
|
||||
| _ := (BinderInfo.default, {ids := []}) /- unreachable, see above -/)
|
||||
| bracketedBinder.View.implicit {content := bc} := pure (BinderInfo.implicit, bc)
|
||||
| bracketedBinder.View.strictImplicit {content := bc} := pure (BinderInfo.strictImplicit, bc)
|
||||
| bracketedBinder.View.instImplicit {content := bc} :=
|
||||
pure $ Prod.mk BinderInfo.instImplicit $ match bc with
|
||||
| instImplicitBinderContent.View.anonymous bca :=
|
||||
{ids := ["_inst_"], type := some {type := bca.type}}
|
||||
| instImplicitBinderContent.View.named bcn :=
|
||||
{ids := [bcn.id], type := some {type := bcn.type}}
|
||||
| bracketedBinder.View.anonymousConstructor ctor :=
|
||||
error (review anonymousConstructor ctor) "unexpected anonymous Constructor",
|
||||
let type := getOptType bc.type,
|
||||
type ← match bc.default with
|
||||
| none := pure type
|
||||
| some (binderDefault.View.val bdv) := pure $ mkApp (globId `optParam) [type, bdv.Term]
|
||||
| some bdv@(binderDefault.View.tac bdt) := match bc.type with
|
||||
| none := pure $ mkApp (globId `autoParam) [bdt.Term]
|
||||
| some _ := error (review binderDefault bdv) "unexpected auto Param after Type annotation",
|
||||
pure $ bc.ids.map (λ bid, mkSimpleBinder (binderIdentToIdent bid) bi type)
|
||||
|
||||
/-- Unfold `binders.View.extended` into `binders.View.simple`. -/
|
||||
def expandBinders (mkBinding : binders.View → Syntax → Syntax) (bnders : binders.View)
|
||||
(body : Syntax) : TransformM (Option Syntax) := do
|
||||
binders.View.extended extBinders ← pure bnders
|
||||
| noExpansion,
|
||||
-- build Result `r` bottom-up
|
||||
let r := body,
|
||||
r ← match extBinders.remainder with
|
||||
| bindersRemainder.View.mixed brms := brms.mfoldr (λ brm r, match brm with
|
||||
-- anonymous Constructor binding ~> binding + match
|
||||
| mixedBinder.View.bracketed (bracketedBinder.View.anonymousConstructor ctor) :=
|
||||
pure $ mkBinding (mkSimpleBinder "x" BinderInfo.default (review hole {})) $ review «match» {
|
||||
scrutinees := [review identUnivs ↑"x"],
|
||||
equations := [{item := {lhs := [review anonymousConstructor ctor], rhs := r}}]
|
||||
}
|
||||
-- local notation: should have been handled by caller, erase
|
||||
| mixedBinder.View.bracketed mbb := do
|
||||
bnders ← expandBracketedBinder mbb,
|
||||
pure $ bnders.foldr (λ bnder, mkBinding bnder) r
|
||||
| mixedBinder.View.id bid := pure $
|
||||
mkBinding (mkSimpleBinder (binderIdentToIdent bid) BinderInfo.default (review hole {})) r
|
||||
) r
|
||||
| _ := pure r,
|
||||
let leadingTy := match extBinders.remainder with
|
||||
| bindersRemainder.View.type brt := brt.type
|
||||
| _ := review hole {},
|
||||
let r := extBinders.leadingIds.foldr (λ bid r,
|
||||
mkBinding (mkSimpleBinder (binderIdentToIdent bid) BinderInfo.default leadingTy) r) r,
|
||||
pure r
|
||||
|
||||
def bracketedBinders.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view bracketedBinders stx,
|
||||
match v with
|
||||
| bracketedBinders.View.simple _ := noExpansion
|
||||
| bracketedBinders.View.extended bnders := do
|
||||
bnders ← bnders.mmap expandBracketedBinder,
|
||||
pure $ review bracketedBinders $ bracketedBinders.View.simple $ List.join bnders
|
||||
|
||||
def lambda.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view lambda stx,
|
||||
expandBinders (λ binders body, review lambda {binders := binders, body := body}) v.binders v.body
|
||||
|
||||
def pi.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view pi stx,
|
||||
expandBinders (λ binders body, review pi {op := v.op, binders := binders, range := body}) v.binders v.range
|
||||
|
||||
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,
|
||||
pure $ review pi {
|
||||
op := Syntax.atom {val := "Π"},
|
||||
binders := binders.View.simple $ simpleBinder.View.explicit {id := `a, type := v.dom},
|
||||
range := v.range}
|
||||
|
||||
def paren.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view paren stx,
|
||||
match v.content with
|
||||
| none := pure $ globId `Unit.unit
|
||||
| some {Term := t, special := none} := pure t
|
||||
| some {Term := t, special := parenSpecial.View.tuple tup} :=
|
||||
pure $ (t::tup.tail.map SepBy.Elem.View.item).foldr1Opt (λ t tup, mkApp (globId `Prod.mk) [t, tup])
|
||||
| some {Term := t, special := parenSpecial.View.typed pst} :=
|
||||
pure $ mkApp (globId `typedExpr) [pst.type, t]
|
||||
|
||||
def assume.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «assume» stx,
|
||||
let binders : binders.View := match v.binders with
|
||||
| assumeBinders.View.anonymous aba := binders.View.simple $
|
||||
-- TODO(Sebastian): unhygienic!
|
||||
simpleBinder.View.explicit {id := "this", type := aba.type}
|
||||
| assumeBinders.View.binders abb := abb,
|
||||
pure $ review lambda {binders := binders, body := v.body}
|
||||
|
||||
def if.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «if» stx,
|
||||
pure $ match v.id with
|
||||
| some id := mkApp (globId `dite) [v.prop,
|
||||
review lambda {binders := binders.View.simple $ simpleBinder.View.explicit {id := id.id, type := v.prop}, body := v.thenBranch},
|
||||
review lambda {binders := binders.View.simple $ simpleBinder.View.explicit {id := id.id, type := mkApp (globId `Not) [v.prop]}, body := v.elseBranch}]
|
||||
| none := mkApp (globId `ite) [v.prop, v.thenBranch, v.elseBranch]
|
||||
|
||||
def let.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «let» stx,
|
||||
match v.lhs with
|
||||
| letLhs.View.id {id := _, binders := [], type := some _} := noExpansion
|
||||
| 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 lli.binders in
|
||||
pure $ review «let» {v with
|
||||
lhs := letLhs.View.id {
|
||||
id := lli.id,
|
||||
binders := [],
|
||||
type := some {type := review pi {op := Syntax.atom {val := "Π"}, binders := bindrs, range := getOptType ty}}},
|
||||
value := review lambda {binders := bindrs, body := v.value}}
|
||||
| letLhs.View.pattern llp :=
|
||||
pure $ review «match» {
|
||||
scrutinees := [v.value],
|
||||
equations := [{item := {lhs := [llp], rhs := v.body}}]}
|
||||
|
||||
-- move parameters into Type
|
||||
def axiom.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «axiom» stx,
|
||||
match v with
|
||||
| {sig := {params := bracketedBinders.View.extended bindrs, type := type}, ..} := do
|
||||
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}}}}
|
||||
| _ := noExpansion
|
||||
|
||||
def declaration.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «declaration» stx,
|
||||
match v.inner with
|
||||
| declaration.inner.View.inductive ind@{«class» := some _, ..} :=
|
||||
let attrs := v.modifiers.attrs.getOrElse {attrs := []} in
|
||||
pure $ review «declaration» {v with
|
||||
modifiers := {v.modifiers with attrs := some {attrs with attrs :=
|
||||
{item := {Name := "class", args := []}} :: attrs.attrs}},
|
||||
inner := declaration.inner.View.inductive {ind with «class» := none}
|
||||
}
|
||||
| declaration.inner.View.structure s@{keyword := structureKw.View.class _, ..} :=
|
||||
let attrs := v.modifiers.attrs.getOrElse {attrs := []} in
|
||||
pure $ review «declaration» {v with
|
||||
modifiers := {v.modifiers with attrs := some {attrs with attrs :=
|
||||
{item := {Name := "class", args := []}} :: attrs.attrs}},
|
||||
inner := declaration.inner.View.structure {s with keyword := structureKw.View.structure}
|
||||
}
|
||||
| _ := noExpansion
|
||||
|
||||
def introRule.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «introRule» stx,
|
||||
match v.sig with
|
||||
| {params := bracketedBinders.View.extended bindrs, type := some type} := do
|
||||
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,
|
||||
range := type.type}}}}
|
||||
| _ := noExpansion
|
||||
|
||||
/- We expand `variable` into `variables` instead of the other way around since, in theory,
|
||||
elaborating multiple variables at the same time makes it possible to omit more information. -/
|
||||
def variable.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «variable» stx,
|
||||
pure $ review «variables» {binders := bracketedBinders.View.extended [v.binder]}
|
||||
|
||||
@[derive HasView]
|
||||
def bindingAnnotationUpdate.Parser : termParser :=
|
||||
node! bindingAnnotationUpdate ["dummy"] -- FIXME: bad node! expansion
|
||||
|
||||
def variables.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «variables» stx,
|
||||
match v.binders with
|
||||
| bracketedBinders.View.simple _ := noExpansion
|
||||
| bracketedBinders.View.extended bnders := do
|
||||
bnders ← bnders.mmap $ λ b, match b with
|
||||
-- binding annotation update
|
||||
| bracketedBinder.View.explicit eb@{content :=
|
||||
explicitBinderContent.View.other bc@{ids := ids, type := none, default := none}} :=
|
||||
expandBracketedBinder $ bracketedBinder.View.explicit {eb with content :=
|
||||
explicitBinderContent.View.other {bc with type := some {type := review bindingAnnotationUpdate {}}}}
|
||||
| _ := expandBracketedBinder b,
|
||||
pure $ review «variables» {binders := bracketedBinders.View.simple $ List.join bnders}
|
||||
|
||||
def Level.leading.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view Level.leading stx,
|
||||
match v with
|
||||
| Level.leading.View.paren p := pure p.inner
|
||||
| _ := noExpansion
|
||||
|
||||
def Subtype.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view Term.Subtype stx,
|
||||
pure $ mkApp (globId `Subtype) [review lambda {
|
||||
binders := mkSimpleBinder v.id BinderInfo.default $ getOptType v.type,
|
||||
body := v.prop
|
||||
}]
|
||||
|
||||
def universes.transform : transformer :=
|
||||
λ stx, do
|
||||
let v := view «universes» stx,
|
||||
pure $ Syntax.list $ v.ids.map (λ id, review «universe» {id := id})
|
||||
|
||||
def sorry.transform : transformer :=
|
||||
λ stx, pure $ mkApp (globId `sorryAx) [review hole {}, globId `Bool.false]
|
||||
|
||||
-- TODO(Sebastian): replace with attribute
|
||||
def builtinTransformers : RBMap Name transformer Name.quickLt := RBMap.fromList [
|
||||
(mixfix.name, mixfix.transform),
|
||||
(reserveMixfix.name, reserveMixfix.transform),
|
||||
(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),
|
||||
(if.name, if.transform),
|
||||
(let.name, let.transform),
|
||||
(axiom.name, axiom.transform),
|
||||
(declaration.name, declaration.transform),
|
||||
(introRule.name, introRule.transform),
|
||||
(variable.name, variable.transform),
|
||||
(variables.name, variables.transform),
|
||||
(Level.leading.name, Level.leading.transform),
|
||||
(Term.Subtype.name, Subtype.transform),
|
||||
(universes.name, universes.transform),
|
||||
(sorry.name, sorry.transform)
|
||||
] _
|
||||
|
||||
structure ExpanderState :=
|
||||
(nextScope : MacroScope)
|
||||
|
||||
structure ExpanderConfig extends TransformerConfig :=
|
||||
(transformers : RBMap Name transformer Name.quickLt)
|
||||
|
||||
instance ExpanderConfig.HasLift : HasLift ExpanderConfig TransformerConfig :=
|
||||
⟨ExpanderConfig.toTransformerConfig⟩
|
||||
|
||||
@[reducible] def ExpanderM := StateT ExpanderState $ ReaderT ExpanderConfig $ ExceptT Message Id
|
||||
|
||||
section
|
||||
local attribute [reducible] MacroScope
|
||||
def ExpanderState.new : ExpanderState := ⟨0⟩
|
||||
def mkScope : ExpanderM MacroScope :=
|
||||
do st ← get,
|
||||
set {st with nextScope := st.nextScope + 1},
|
||||
pure st.nextScope
|
||||
end
|
||||
|
||||
private def expandCore : Nat → Syntax → ExpanderM Syntax
|
||||
| 0 stx := error stx "macro expansion limit exceeded"
|
||||
| (fuel + 1) stx :=
|
||||
do some n ← pure stx.asNode | pure stx,
|
||||
cfg ← read,
|
||||
some t ← pure $ cfg.transformers.find n.kind.name
|
||||
-- not a macro: recurse
|
||||
| Syntax.mkNode n.kind <$> n.args.mmap (expandCore fuel),
|
||||
sc ← mkScope,
|
||||
let n' := Syntax.mkNode n.kind $ n.args.map (Syntax.flipScopes [sc]),
|
||||
some stx' ← StateT.lift $ λ cfg, t n' ↑cfg
|
||||
-- no unfolding: recurse
|
||||
| Syntax.mkNode n.kind <$> n.args.mmap (expandCore fuel),
|
||||
-- flip again, expand iteratively
|
||||
expandCore fuel $ stx'.flipScopes [sc]
|
||||
|
||||
def expand (stx : Syntax) : ReaderT ExpanderConfig (Except Message) Syntax :=
|
||||
-- TODO(Sebastian): persist macro scopes across commands/files
|
||||
Prod.fst <$> expandCore 1000 stx ExpanderState.new
|
||||
|
||||
end Expander
|
||||
end Lean
|
||||
|
|
@ -1,91 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
-/
|
||||
|
||||
import init.lean.parser.module init.lean.expander init.lean.elaborator init.lean.util init.io
|
||||
|
||||
namespace Lean
|
||||
open Lean.Parser
|
||||
open Lean.Expander
|
||||
open Lean.Elaborator
|
||||
|
||||
def mkConfig (filename := "<unknown>") (input := "") : Except String ModuleParserConfig :=
|
||||
do t ← Parser.mkTokenTrie $
|
||||
Parser.tokens Module.header.Parser ++
|
||||
Parser.tokens command.builtinCommandParsers ++
|
||||
Parser.tokens Term.builtinLeadingParsers ++
|
||||
Parser.tokens Term.builtinTrailingParsers,
|
||||
pure $ {
|
||||
filename := filename, input := input, tokens := t,
|
||||
fileMap := FileMap.fromString input,
|
||||
commandParsers := command.builtinCommandParsers,
|
||||
leadingTermParsers := Term.builtinLeadingParsers,
|
||||
trailingTermParsers := Term.builtinTrailingParsers,
|
||||
}
|
||||
|
||||
def runFrontend (filename input : String) (printMsg : Message → IO Unit) (collectOutputs : Bool) :
|
||||
StateT Environment IO (List Syntax) := λ env, do
|
||||
parserCfg ← ioOfExcept $ mkConfig filename input,
|
||||
-- TODO(Sebastian): `parseHeader` should be called directly by Lean.cpp
|
||||
match parseHeader parserCfg with
|
||||
| (_, Except.error msg) := printMsg msg *> pure ([], env)
|
||||
| (_, Except.ok (pSnap, msgs)) := do
|
||||
msgs.toList.mfor printMsg,
|
||||
let expanderCfg : ExpanderConfig := {transformers := builtinTransformers, ..parserCfg},
|
||||
let elabCfg : ElaboratorConfig := {filename := filename, input := input, initialParserCfg := parserCfg, ..parserCfg},
|
||||
let opts := Options.empty.setBool `trace.as_messages true,
|
||||
let elabSt := Elaborator.mkState elabCfg env opts,
|
||||
let addOutput (out : Syntax) outs := if collectOutputs then out::outs else [],
|
||||
IO.Prim.iterate (pSnap, elabSt, parserCfg, expanderCfg, ([] : List Syntax)) $ λ ⟨pSnap, elabSt, parserCfg, expanderCfg, outs⟩, do {
|
||||
let pos := parserCfg.fileMap.toPosition pSnap.it.offset,
|
||||
r ← monadLift $ profileitPure "parsing" pos $ λ _, parseCommand parserCfg pSnap,
|
||||
match r with
|
||||
| (cmd, Except.error msg) := do {
|
||||
-- fatal error (should never happen?)
|
||||
printMsg msg,
|
||||
msgs.toList.mfor printMsg,
|
||||
pure $ Sum.inr ((addOutput cmd outs).reverse, elabSt.env)
|
||||
}
|
||||
| (cmd, Except.ok (pSnap, msgs)) := do {
|
||||
msgs.toList.mfor printMsg,
|
||||
r ← monadLift $ profileitPure "expanding" pos $ λ _, (expand cmd).run expanderCfg,
|
||||
match r with
|
||||
| Except.ok cmd' := do {
|
||||
--IO.println cmd',
|
||||
elabSt ← monadLift $ profileitPure "elaborating" pos $ λ _, Elaborator.processCommand elabCfg elabSt cmd',
|
||||
elabSt.messages.toList.mfor printMsg,
|
||||
if cmd'.isOfKind Module.eoi then
|
||||
/-printMsg {filename := filename, severity := MessageSeverity.information,
|
||||
pos := ⟨1, 0⟩,
|
||||
text := "Parser cache hit rate: " ++ toString out.cache.hit ++ "/" ++
|
||||
toString (out.cache.hit + out.cache.miss)},-/
|
||||
pure $ Sum.inr ((addOutput cmd outs).reverse, elabSt.env)
|
||||
else
|
||||
pure (Sum.inl (pSnap, elabSt, elabSt.parserCfg, elabSt.expanderCfg, addOutput cmd outs))
|
||||
}
|
||||
| Except.error e := printMsg e *> pure (Sum.inl (pSnap, elabSt, parserCfg, expanderCfg, addOutput cmd outs))
|
||||
}
|
||||
}
|
||||
|
||||
@[export lean_process_file]
|
||||
def processFile (f s : String) (json : Bool) : StateT Environment IO Unit := do
|
||||
let printMsg : Message → IO Unit := λ msg,
|
||||
if json then
|
||||
IO.println $ "{\"file_name\": \"<stdin>\", \"pos_line\": " ++ toString msg.pos.line ++
|
||||
", \"pos_col\": " ++ toString msg.pos.column ++
|
||||
", \"severity\": " ++ repr (match msg.severity with
|
||||
| MessageSeverity.information := "information"
|
||||
| MessageSeverity.warning := "warning"
|
||||
| MessageSeverity.error := "error") ++
|
||||
", \"caption\": " ++ repr msg.caption ++
|
||||
", \"text\": " ++ repr msg.text ++ "}"
|
||||
else IO.println msg.toString,
|
||||
-- print and erase uncaught exceptions
|
||||
catch
|
||||
(runFrontend f s printMsg false *> pure ())
|
||||
(λ e, do
|
||||
monadLift (printMsg {filename := f, severity := MessageSeverity.error, pos := ⟨1, 0⟩, text := e}),
|
||||
throw e)
|
||||
end Lean
|
||||
|
|
@ -1,226 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Parser for the Lean language
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.parsec init.lean.parser.syntax init.lean.parser.rec
|
||||
import init.lean.parser.trie
|
||||
import init.lean.parser.identifier init.data.rbmap init.lean.message
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
/- Maximum standard precedence. This is the precedence of Function application.
|
||||
In the standard Lean language, only the token `.` has a left-binding power greater
|
||||
than `maxPrec` (so that field accesses like `g (h x).f` are parsed as `g ((h x).f)`,
|
||||
not `(g (h x)).f`). -/
|
||||
def maxPrec : Nat := 1024
|
||||
|
||||
structure TokenConfig :=
|
||||
(«prefix» : String)
|
||||
/- Left-binding power used by the Term Parser. The Term Parser operates in the context
|
||||
of a right-binding power between 0 (used by parentheses and on the top-Level) and
|
||||
(usually) `maxPrec` (used by Function application). After parsing an initial Term,
|
||||
it continues parsing and expanding that Term only when the left-binding power of
|
||||
the next token is greater than the current right-binding power. For example, it
|
||||
never continues parsing an argument after the initial parse, unless a token with
|
||||
lbp > maxPrec is encountered. Conversely, the Term Parser will always continue
|
||||
parsing inside parentheses until it finds a token with lbp 0 (such as `)`). -/
|
||||
(lbp : Nat := 0)
|
||||
-- reading a token should not need any State
|
||||
/- An optional Parser that is activated after matching `prefix`.
|
||||
It should return a Syntax tree with a "hole" for the
|
||||
`SourceInfo` surrounding the token, which will be supplied
|
||||
by the `token` Parser.
|
||||
|
||||
Remark: `suffixParser` has many applications for example for parsing
|
||||
hexdecimal numbers, `prefix` is `0x` and `suffixParser` is the Parser `digit*`.
|
||||
We also use it to parse String literals: here `prefix` is just `"`.
|
||||
-/
|
||||
(suffixParser : Option (Parsec' (SourceInfo → Syntax)) := none)
|
||||
|
||||
-- Backtrackable State
|
||||
structure ParserState :=
|
||||
(messages : MessageLog)
|
||||
|
||||
structure TokenCacheEntry :=
|
||||
(startIt stopIt : String.OldIterator)
|
||||
(tk : Syntax)
|
||||
|
||||
-- Non-backtrackable State
|
||||
structure ParserCache :=
|
||||
(tokenCache : Option TokenCacheEntry := none)
|
||||
-- for profiling
|
||||
(hit miss : Nat := 0)
|
||||
|
||||
structure FrontendConfig :=
|
||||
(filename : String)
|
||||
(input : String)
|
||||
(fileMap : FileMap)
|
||||
|
||||
/- Remark: if we have a Node in the Trie with `some TokenConfig`, the String induced by the path is equal to the `TokenConfig.prefix`. -/
|
||||
structure ParserConfig extends FrontendConfig :=
|
||||
(tokens : Trie TokenConfig)
|
||||
|
||||
instance parserConfigCoe : HasCoe ParserConfig FrontendConfig :=
|
||||
⟨ParserConfig.toFrontendConfig⟩
|
||||
|
||||
@[derive Monad Alternative MonadParsec MonadExcept]
|
||||
def parserCoreT (m : Type → Type) [Monad m] :=
|
||||
ParsecT Syntax $ StateT ParserCache $ m
|
||||
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept]
|
||||
def ParserT (ρ : Type) (m : Type → Type) [Monad m] := ReaderT ρ $ parserCoreT m
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept]
|
||||
def BasicParserM := ParserT ParserConfig Id
|
||||
abbrev basicParser := BasicParserM Syntax
|
||||
abbrev monadBasicParser := HasMonadLiftT BasicParserM
|
||||
|
||||
section
|
||||
local attribute [reducible] BasicParserM ParserT parserCoreT
|
||||
@[inline] def getCache : BasicParserM ParserCache :=
|
||||
monadLift (get : StateT ParserCache Id _)
|
||||
|
||||
@[inline] def putCache : ParserCache → BasicParserM PUnit :=
|
||||
λ c, monadLift (set c : StateT ParserCache Id _)
|
||||
end
|
||||
|
||||
-- an arbitrary `Parser` Type; parsers are usually some Monad stack based on `BasicParserM` returning `Syntax`
|
||||
variable {ρ : Type}
|
||||
|
||||
class HasTokens (r : ρ) := mk {} ::
|
||||
(tokens : List TokenConfig)
|
||||
|
||||
@[noinline, nospecialize] def tokens (r : ρ) [HasTokens r] :=
|
||||
HasTokens.tokens r
|
||||
|
||||
instance HasTokens.Inhabited (r : ρ) : Inhabited (HasTokens r) :=
|
||||
⟨⟨[]⟩⟩
|
||||
|
||||
instance List.nil.tokens : Parser.HasTokens ([] : List ρ) :=
|
||||
default _
|
||||
|
||||
instance List.cons.tokens (r : ρ) (rs : List ρ) [Parser.HasTokens r] [Parser.HasTokens rs] :
|
||||
Parser.HasTokens (r::rs) :=
|
||||
⟨tokens r ++ tokens rs⟩
|
||||
|
||||
class HasView (α : outParam Type) (r : ρ) :=
|
||||
(view : Syntax → α)
|
||||
(review : α → Syntax)
|
||||
|
||||
export HasView (view review)
|
||||
|
||||
def tryView {α : Type} (k : SyntaxNodeKind) [HasView α k] (stx : Syntax) : Option α :=
|
||||
if stx.isOfKind k then some (HasView.view k stx) else none
|
||||
|
||||
instance HasView.default (r : ρ) : Inhabited (Parser.HasView Syntax r) :=
|
||||
⟨{ view := id, review := id }⟩
|
||||
|
||||
class HasViewDefault (r : ρ) (α : outParam Type) [HasView α r] (default : α) := mk {}
|
||||
|
||||
def messageOfParsecMessage {μ : Type} (cfg : FrontendConfig) (msg : Parsec.Message μ) : Message :=
|
||||
{filename := cfg.filename, pos := cfg.fileMap.toPosition msg.it.offset, text := msg.text}
|
||||
|
||||
/-- Run Parser stack, returning a partial Syntax tree in case of a fatal error -/
|
||||
protected def run {m : Type → Type} {α ρ : Type} [Monad m] [HasCoeT ρ FrontendConfig] (cfg : ρ) (s : String) (r : StateT ParserState (ParserT ρ m) α) :
|
||||
m (Sum α Syntax × MessageLog) :=
|
||||
do (r, _) ← (((r.run {messages:=MessageLog.empty}).run cfg).parse s).run {},
|
||||
pure $ match r with
|
||||
| Except.ok (a, st) := (Sum.inl a, st.messages)
|
||||
| Except.error msg := (Sum.inr msg.custom.get, MessageLog.empty.add (messageOfParsecMessage cfg msg))
|
||||
|
||||
open MonadParsec
|
||||
open Parser.HasView
|
||||
variables {α : Type} {m : Type → Type}
|
||||
local notation `Parser` := m Syntax
|
||||
|
||||
def logMessage {μ : Type} [Monad m] [MonadReader ρ m] [HasLiftT ρ FrontendConfig] [MonadState ParserState m]
|
||||
(msg : Parsec.Message μ) : m Unit :=
|
||||
do cfg ← read,
|
||||
modify (λ st, {st with messages := st.messages.add (messageOfParsecMessage ↑cfg msg)})
|
||||
|
||||
def mkTokenTrie (tokens : List TokenConfig) : Except String (Trie TokenConfig) :=
|
||||
do -- the only hardcoded tokens, because they are never directly mentioned by a `Parser`
|
||||
let builtinTokens : List TokenConfig := [{«prefix» := "/-"}, {«prefix» := "--"}],
|
||||
t ← (builtinTokens ++ tokens).mfoldl (λ (t : Trie TokenConfig) tk,
|
||||
match t.find tk.prefix with
|
||||
| some tk' := match tk.lbp, tk'.lbp with
|
||||
| l, 0 := pure $ t.insert tk.prefix tk
|
||||
| 0, _ := pure t
|
||||
| l, l' := if l = l' then pure t else throw $
|
||||
"invalid token '" ++ tk.prefix ++ "', has been defined with precedences " ++
|
||||
toString l ++ " and " ++ toString l'
|
||||
| none := pure $ t.insert tk.prefix tk)
|
||||
Trie.empty,
|
||||
pure t
|
||||
|
||||
|
||||
/- Monad stacks used in multiple files -/
|
||||
|
||||
/- NOTE: We move `RecT` under `ParserT`'s `ReaderT` so that `termParser`, which does not
|
||||
have access to `commandParser`'s ρ (=`CommandParserConfig`) can still recurse into it
|
||||
(for command quotations). This means that the `CommandParserConfig` will be reset
|
||||
on a recursive call to `command.Parser`, i.e. it forgets about locally registered parsers,
|
||||
but that's not an issue for our intended uses of it. -/
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept MonadRec]
|
||||
def CommandParserM (ρ : Type) := ReaderT ρ $ RecT Unit Syntax $ parserCoreT Id
|
||||
|
||||
section
|
||||
local attribute [reducible] ParserT CommandParserM
|
||||
instance CommandParserM.MonadReaderAdapter (ρ ρ' : Type) :
|
||||
MonadReaderAdapter ρ ρ' (CommandParserM ρ) (CommandParserM ρ') :=
|
||||
inferInstance
|
||||
instance CommandParserM.basicParser (ρ : Type) [HasLiftT ρ ParserConfig] : monadBasicParser (CommandParserM ρ) :=
|
||||
⟨λ _ x cfg rec, x.run ↑cfg⟩
|
||||
end
|
||||
|
||||
/- The `Nat` at `RecT` is the lbp` -/
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept MonadRec monadBasicParser]
|
||||
def TermParserM := RecT Nat Syntax $ CommandParserM ParserConfig
|
||||
abbrev termParser := TermParserM Syntax
|
||||
|
||||
/-- A Term Parser for a suffix or infix notation that accepts a preceding Term. -/
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept MonadRec monadBasicParser]
|
||||
def TrailingTermParserM := ReaderT Syntax TermParserM
|
||||
abbrev trailingTermParser := TrailingTermParserM Syntax
|
||||
|
||||
instance trailingTermParserCoe : HasCoe termParser trailingTermParser :=
|
||||
⟨λ x _, x⟩
|
||||
|
||||
/-- A multimap indexed by tokens. Used for indexing parsers by their leading token. -/
|
||||
def TokenMap (α : Type) := RBMap Name (List α) Name.quickLt
|
||||
|
||||
def TokenMap.insert {α : Type} (map : TokenMap α) (k : Name) (v : α) : TokenMap α :=
|
||||
match map.find k with
|
||||
| none := map.insert k [v]
|
||||
| some vs := map.insert k (v::vs)
|
||||
|
||||
def TokenMap.ofList {α : Type} : List (Name × α) → TokenMap α
|
||||
| [] := mkRBMap _ _ _
|
||||
| (⟨k,v⟩::xs) := (TokenMap.ofList xs).insert k v
|
||||
|
||||
instance tokenMapNil.tokens : Parser.HasTokens $ @TokenMap.ofList ρ [] :=
|
||||
default _
|
||||
|
||||
instance tokenMapCons.tokens (k : Name) (r : ρ) (rs : List (Name × ρ)) [Parser.HasTokens r] [Parser.HasTokens $ TokenMap.ofList rs] :
|
||||
Parser.HasTokens $ TokenMap.ofList ((k,r)::rs) :=
|
||||
⟨tokens r ++ tokens (TokenMap.ofList rs)⟩
|
||||
|
||||
-- This needs to be a separate structure since `termParser`s cannot contain themselves in their config
|
||||
structure CommandParserConfig extends ParserConfig :=
|
||||
(leadingTermParsers : TokenMap termParser)
|
||||
(trailingTermParsers : TokenMap trailingTermParser)
|
||||
-- local Term parsers (such as from `local notation`) hide previous parsers instead of overloading them
|
||||
(localLeadingTermParsers : TokenMap termParser := mkRBMap _ _ _)
|
||||
(localTrailingTermParsers : TokenMap trailingTermParser := mkRBMap _ _ _)
|
||||
|
||||
instance commandParserConfigCoeParserConfig : HasCoe CommandParserConfig ParserConfig :=
|
||||
⟨CommandParserConfig.toParserConfig⟩
|
||||
|
||||
abbrev commandParser := CommandParserM CommandParserConfig Syntax
|
||||
|
||||
end «Parser»
|
||||
end Lean
|
||||
|
|
@ -1,247 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Syntax-tree creating Parser Combinators
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.basic
|
||||
import init.data.list.instances
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
namespace Combinators
|
||||
open HasTokens HasView MonadParsec
|
||||
|
||||
variables {α : Type} {m : Type → Type}
|
||||
local notation `Parser` := m Syntax
|
||||
variables [Monad m] [MonadExcept (Parsec.Message Syntax) m] [MonadParsec Syntax m] [Alternative m]
|
||||
|
||||
def node (k : SyntaxNodeKind) (rs : List Parser) : Parser :=
|
||||
do args ← rs.mfoldl (λ (args : List Syntax) r, do
|
||||
-- on error, append partial Syntax tree to previous successful parses and rethrow
|
||||
a ← catch r $ λ msg, match args with
|
||||
-- do not wrap an error in the first argument to uphold the invariant documented at `SyntaxNode`
|
||||
| [] := throw msg
|
||||
| _ :=
|
||||
let args := msg.custom.get :: args in
|
||||
throw {msg with custom := Syntax.mkNode k args.reverse},
|
||||
pure (a::args)
|
||||
) [],
|
||||
pure $ Syntax.mkNode k args.reverse
|
||||
|
||||
@[reducible] def seq : List Parser → Parser := node noKind
|
||||
|
||||
instance node.tokens (k) (rs : List Parser) [Parser.HasTokens rs] : Parser.HasTokens (node k rs) :=
|
||||
⟨tokens rs⟩
|
||||
|
||||
instance node.view (k) (rs : List Parser) [i : HasView α k] : Parser.HasView α (node k rs) :=
|
||||
{ view := i.view, review := i.review }
|
||||
|
||||
-- Each Parser Combinator comes equipped with `HasView` and `HasTokens` instances
|
||||
|
||||
private def many1Aux (p : Parser) : List Syntax → Nat → Parser
|
||||
| as 0 := error "unreachable"
|
||||
| as (n+1) := do
|
||||
a ← catch p (λ msg, throw {msg with custom :=
|
||||
-- append `Syntax.missing` to make clear that List is incomplete
|
||||
Syntax.list (Syntax.missing::msg.custom.get::as).reverse}),
|
||||
many1Aux (a::as) n <|> pure (Syntax.list (a::as).reverse)
|
||||
|
||||
def many1 (r : Parser) : Parser :=
|
||||
do rem ← remaining, many1Aux r [] (rem+1)
|
||||
|
||||
instance many1.tokens (r : Parser) [Parser.HasTokens r] : Parser.HasTokens (many1 r) :=
|
||||
⟨tokens r⟩
|
||||
|
||||
instance many1.view (r : Parser) [Parser.HasView α r] : Parser.HasView (List α) (many1 r) :=
|
||||
{ view := λ stx, match stx.asNode with
|
||||
| some n := n.args.map (HasView.view r)
|
||||
| _ := [HasView.view r Syntax.missing],
|
||||
review := λ as, Syntax.list $ as.map (review r) }
|
||||
|
||||
def many (r : Parser) : Parser :=
|
||||
many1 r <|> pure (Syntax.list [])
|
||||
|
||||
instance many.tokens (r : Parser) [Parser.HasTokens r] : Parser.HasTokens (many r) :=
|
||||
⟨tokens r⟩
|
||||
|
||||
instance many.view (r : Parser) [HasView α r] : Parser.HasView (List α) (many r) :=
|
||||
/- Remark: `many1.view` can handle empty list. -/
|
||||
{..many1.view r}
|
||||
|
||||
private def sepByAux (p : m Syntax) (sep : Parser) (allowTrailingSep : Bool) : Bool → List Syntax → Nat → Parser
|
||||
| pOpt as 0 := error "unreachable"
|
||||
| pOpt as (n+1) := do
|
||||
let p := if pOpt then some <$> p <|> pure none else some <$> p,
|
||||
some a ← catch p (λ msg, throw {msg with custom :=
|
||||
-- append `Syntax.missing` to make clear that List is incomplete
|
||||
Syntax.list (Syntax.missing::msg.custom.get::as).reverse})
|
||||
| pure (Syntax.list as.reverse),
|
||||
-- I don't want to think about what the output on a failed separator parse should look like
|
||||
let sep := try sep,
|
||||
some s ← some <$> sep <|> pure none
|
||||
| pure (Syntax.list (a::as).reverse),
|
||||
sepByAux allowTrailingSep (s::a::as) n
|
||||
|
||||
def sepBy (p sep : Parser) (allowTrailingSep := true) : Parser :=
|
||||
do rem ← remaining, sepByAux p sep allowTrailingSep true [] (rem+1)
|
||||
|
||||
def sepBy1 (p sep : Parser) (allowTrailingSep := true) : Parser :=
|
||||
do rem ← remaining, sepByAux p sep allowTrailingSep false [] (rem+1)
|
||||
|
||||
instance sepBy.tokens (p sep : Parser) (a) [Parser.HasTokens p] [Parser.HasTokens sep] :
|
||||
Parser.HasTokens (sepBy p sep a) :=
|
||||
⟨tokens p ++ tokens sep⟩
|
||||
|
||||
structure SepBy.Elem.View (α β : Type) :=
|
||||
(item : α)
|
||||
(separator : Option β := none)
|
||||
|
||||
instance SepBy.Elem.View.itemCoe {α β : Type} : HasCoeT α (SepBy.Elem.View α β) :=
|
||||
⟨λ a, ⟨a, none⟩⟩
|
||||
|
||||
private def sepBy.viewAux {α β} (p sep : Parser) [Parser.HasView α p] [Parser.HasView β sep] :
|
||||
List Syntax → List (SepBy.Elem.View α β)
|
||||
| [] := []
|
||||
| [stx] := [⟨HasView.view p stx, none⟩]
|
||||
| (stx1::stx2::stxs) := ⟨HasView.view p stx1, some $ HasView.view sep stx2⟩::sepBy.viewAux stxs
|
||||
|
||||
instance sepBy.view {α β} (p sep : Parser) (a) [Parser.HasView α p] [Parser.HasView β sep] :
|
||||
Parser.HasView (List (SepBy.Elem.View α β)) (sepBy p sep a) :=
|
||||
{ view := λ stx, match stx.asNode with
|
||||
| some n := sepBy.viewAux p sep n.args
|
||||
| _ := [⟨view p Syntax.missing, none⟩],
|
||||
review := λ as, Syntax.list $ as.bind (λ a, match a with
|
||||
| ⟨v, some vsep⟩ := [review p v, review sep vsep]
|
||||
| ⟨v, none⟩ := [review p v]) }
|
||||
|
||||
instance sepBy1.tokens (p sep : Parser) (a) [Parser.HasTokens p] [Parser.HasTokens sep] :
|
||||
Parser.HasTokens (sepBy1 p sep a) :=
|
||||
⟨tokens (sepBy p sep a)⟩
|
||||
|
||||
instance sepBy1.View {α β} (p sep : Parser) (a) [Parser.HasView α p] [Parser.HasView β sep] :
|
||||
Parser.HasView (List (SepBy.Elem.View α β)) (sepBy1 p sep a) :=
|
||||
{..sepBy.view p sep a}
|
||||
|
||||
/-- Optionally parse `r`. `require` can be used to conditionally override the
|
||||
behavior without changing the structure of the syntax tree. -/
|
||||
def optional (r : Parser) (require := false) : Parser :=
|
||||
if require then r else
|
||||
do r ← optional $
|
||||
-- on error, wrap in "some"
|
||||
catch r (λ msg, throw {msg with custom := Syntax.list [msg.custom.get]}),
|
||||
pure $ match r with
|
||||
| some r := Syntax.list [r]
|
||||
| none := Syntax.list []
|
||||
|
||||
instance optional.tokens (r : Parser) [Parser.HasTokens r] (req) : Parser.HasTokens (optional r req) :=
|
||||
⟨tokens r⟩
|
||||
instance optional.view (r : Parser) [Parser.HasView α r] (req) : Parser.HasView (Option α) (optional r req) :=
|
||||
{ view := λ stx, match stx.asNode with
|
||||
| some {args := [], ..} := none
|
||||
| some {args := [stx], ..} := some $ HasView.view r stx
|
||||
| _ := some $ view r Syntax.missing,
|
||||
review := λ a, match a with
|
||||
| some a := Syntax.list [review r a]
|
||||
| none := Syntax.list [] }
|
||||
instance optional.viewDefault (r : Parser) [Parser.HasView α r] (req) : Parser.HasViewDefault (optional r req) (Option α) none := ⟨⟩
|
||||
|
||||
/-- Parse a List `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
|
||||
Note that there is NO explicit encoding of which Parser was chosen;
|
||||
parsers should instead produce distinct Node names for disambiguation. -/
|
||||
def anyOf (rs : List Parser) : Parser :=
|
||||
match rs with
|
||||
| [] := error "anyOf"
|
||||
| (r::rs) := rs.foldl (<|>) r
|
||||
|
||||
instance anyOf.tokens (rs : List Parser) [Parser.HasTokens rs] : Parser.HasTokens (anyOf rs) :=
|
||||
⟨tokens rs⟩
|
||||
instance anyOf.view (rs : List Parser) : Parser.HasView Syntax (anyOf rs) := default _
|
||||
|
||||
/-- Parse a List `[p1, ..., pn]` of parsers with `MonadParsec.longestMatch`.
|
||||
If the Result is ambiguous, wrap it in a `choice` Node.
|
||||
Note that there is NO explicit encoding of which Parser was chosen;
|
||||
parsers should instead produce distinct Node names for disambiguation. -/
|
||||
def longestMatch (rs : List Parser) : Parser :=
|
||||
do stxs ← MonadParsec.longestMatch rs,
|
||||
match stxs with
|
||||
| [stx] := pure stx
|
||||
| _ := pure $ Syntax.mkNode choice stxs
|
||||
|
||||
instance longestMatch.tokens (rs : List Parser) [Parser.HasTokens rs] : Parser.HasTokens (longestMatch rs) :=
|
||||
⟨tokens rs⟩
|
||||
instance longestMatch.view (rs : List Parser) : Parser.HasView Syntax (longestMatch rs) := default _
|
||||
|
||||
def choiceAux : List Parser → Nat → Parser
|
||||
| [] _ := error "choice: Empty List"
|
||||
| (r::rs) i :=
|
||||
do { stx ← r,
|
||||
pure $ Syntax.mkNode ⟨Name.mkNumeral Name.anonymous i⟩ [stx] }
|
||||
<|> choiceAux rs (i+1)
|
||||
|
||||
/-- Parse a List `[p1, ..., pn]` of parsers as `p1 <|> ... <|> pn`.
|
||||
The Result will be wrapped in a Node with the index of the successful
|
||||
Parser as the Name.
|
||||
|
||||
Remark: Does not have a `HasView` instance because we only use it in `nodeChoice!` macros
|
||||
that define their own views. -/
|
||||
def choice (rs : List Parser) : Parser :=
|
||||
choiceAux rs 0
|
||||
|
||||
instance choice.tokens (rs : List Parser) [Parser.HasTokens rs] : Parser.HasTokens (choice rs) :=
|
||||
⟨tokens rs⟩
|
||||
|
||||
/-- Like `choice`, but using `longestMatch`. Does not create choice nodes, prefers the first successful Parser. -/
|
||||
def longestChoice (rs : List Parser) : Parser :=
|
||||
do stx::stxs ← MonadParsec.longestMatch $ rs.enum.map $ λ ⟨i, r⟩, do {
|
||||
stx ← r,
|
||||
pure $ Syntax.mkNode ⟨Name.mkNumeral Name.anonymous i⟩ [stx]
|
||||
} | error "unreachable",
|
||||
pure stx
|
||||
|
||||
instance longestChoice.tokens (rs : List Parser) [Parser.HasTokens rs] : Parser.HasTokens (longestChoice rs) :=
|
||||
|
||||
⟨tokens rs⟩
|
||||
instance try.tokens (r : Parser) [Parser.HasTokens r] : Parser.HasTokens (try r) :=
|
||||
⟨tokens r⟩
|
||||
instance try.view (r : Parser) [i : Parser.HasView α r] : Parser.HasView α (try r) :=
|
||||
{..i}
|
||||
|
||||
instance label.tokens (r : Parser) (l) [Parser.HasTokens r] : Parser.HasTokens (label r l) :=
|
||||
⟨tokens r⟩
|
||||
instance label.view (r : Parser) (l) [i : Parser.HasView α r] : Parser.HasView α (label r l) :=
|
||||
{..i}
|
||||
|
||||
instance recurse.tokens (α δ m a) [MonadRec α δ m] : Parser.HasTokens (recurse a : m δ) :=
|
||||
default _ -- recursive use should not contribute any new tokens
|
||||
instance recurse.view (α δ m a) [MonadRec α δ m] : Parser.HasView Syntax (recurse a : m δ) := default _
|
||||
|
||||
instance monadLift.tokens {m' : Type → Type} [HasMonadLiftT m m'] (r : m Syntax) [Parser.HasTokens r] :
|
||||
Parser.HasTokens (monadLift r : m' Syntax) :=
|
||||
⟨tokens r⟩
|
||||
instance monadLift.view {m' : Type → Type} [HasMonadLiftT m m'] (r : m Syntax) [i : Parser.HasView α r] :
|
||||
Parser.HasView α (monadLift r : m' Syntax) :=
|
||||
{..i}
|
||||
|
||||
instance seqLeft.tokens {α : Type} (x : m α) (p : m Syntax) [Parser.HasTokens p] : Parser.HasTokens (p <* x) :=
|
||||
⟨tokens p⟩
|
||||
instance seqLeft.view {α β : Type} (x : m α) (p : m Syntax) [i : Parser.HasView β p] : Parser.HasView β (p <* x) :=
|
||||
{..i}
|
||||
|
||||
instance seqRight.tokens {α : Type} (x : m α) (p : m Syntax) [Parser.HasTokens p] : Parser.HasTokens (x *> p) :=
|
||||
⟨tokens p⟩
|
||||
instance seqRight.view {α β : Type} (x : m α) (p : m Syntax) [i : Parser.HasView β p] : Parser.HasView β (x *> p) :=
|
||||
{..i}
|
||||
|
||||
instance coe.tokens {β} (r : Parser) [Parser.HasTokens r] [HasCoeT Parser β]: Parser.HasTokens (coe r : β) :=
|
||||
⟨tokens r⟩
|
||||
instance coe.view {β} (r : Parser) [i : Parser.HasView α r] [HasCoeT Parser β] : Parser.HasView α (coe r : β) :=
|
||||
{..i}
|
||||
instance coe.viewDefault {β} (d : α) (r : Parser) [HasView α r] [Parser.HasViewDefault r α d] [HasCoeT Parser β] : Parser.HasViewDefault (coe r : β) α d := ⟨⟩
|
||||
|
||||
end Combinators
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,165 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Command parsers
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.declaration
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
open Combinators MonadParsec
|
||||
open Parser.HasTokens Parser.HasView
|
||||
|
||||
local postfix `?`:10000 := optional
|
||||
local postfix *:10000 := Combinators.many
|
||||
local postfix +:10000 := Combinators.many1
|
||||
|
||||
set_option class.instance_max_depth 300
|
||||
|
||||
@[derive Parser.HasView Parser.HasTokens]
|
||||
def command.Parser : commandParser :=
|
||||
recurse () <?> "command"
|
||||
|
||||
namespace «command»
|
||||
|
||||
@[derive Parser.HasView Parser.HasTokens]
|
||||
def openSpec.Parser : commandParser :=
|
||||
node! openSpec [
|
||||
id: ident.Parser,
|
||||
as: node! openSpec.as ["as", id: ident.Parser]?,
|
||||
only: node! openSpec.only [try ["(", id: ident.Parser], ids: ident.Parser*, ")"]?,
|
||||
«renaming»: node! openSpec.renaming [try ["(", "renaming"], items: node! openSpec.renaming.item [«from»: ident.Parser, "->", to: ident.Parser]+, ")"]?,
|
||||
«hiding»: node! openSpec.hiding ["(", "hiding", ids: ident.Parser+, ")"]?
|
||||
]+
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def open.Parser : commandParser :=
|
||||
node! «open» ["open", spec: openSpec.Parser]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def export.Parser : commandParser :=
|
||||
node! «export» ["export", spec: openSpec.Parser]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def section.Parser : commandParser :=
|
||||
node! «section» ["section", Name: ident.Parser?]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def namespace.Parser : commandParser :=
|
||||
node! «namespace» ["namespace", Name: ident.Parser]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def variable.Parser : commandParser :=
|
||||
node! «variable» ["variable", binder: Term.binder.Parser]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def variables.Parser : commandParser :=
|
||||
-- TODO: should require at least one binder
|
||||
node! «variables» ["variables", binders: Term.bracketedBinders.Parser]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def include.Parser : commandParser :=
|
||||
node! «include» ["include ", ids: ident.Parser+]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def omit.Parser : commandParser :=
|
||||
node! «omit» ["omit ", ids: ident.Parser+]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def end.Parser : commandParser :=
|
||||
node! «end» ["end", Name: ident.Parser?]
|
||||
|
||||
@[derive Parser.HasTokens]
|
||||
def universe.Parser : commandParser :=
|
||||
anyOf [
|
||||
node! «universes» ["universes", ids: ident.Parser+],
|
||||
node! «universe» ["universe", id: ident.Parser]
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def check.Parser : commandParser :=
|
||||
node! check ["#check", Term: Term.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def attribute.Parser : commandParser :=
|
||||
node! «attribute» [
|
||||
try [«local»: (symbol "local ")?, "attribute "],
|
||||
"[",
|
||||
attrs: sepBy1 attrInstance.Parser (symbol ", "),
|
||||
"] ",
|
||||
ids: ident.Parser*
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def initQuot.Parser : commandParser :=
|
||||
node! «initQuot» ["initQuot"]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def setOption.Parser : commandParser :=
|
||||
node! «setOption» ["setOption", opt: ident.Parser, val: nodeChoice! optionValue {
|
||||
Bool: nodeChoice! boolOptionValue {
|
||||
True: symbolOrIdent "true",
|
||||
False: symbolOrIdent "false",
|
||||
},
|
||||
String: stringLit.Parser,
|
||||
-- TODO(Sebastian): fractional numbers
|
||||
num: number.Parser,
|
||||
}]
|
||||
|
||||
@[derive HasTokens]
|
||||
def builtinCommandParsers : TokenMap commandParser := TokenMap.ofList [
|
||||
("/--", declaration.Parser),
|
||||
("@[", declaration.Parser),
|
||||
("private", declaration.Parser),
|
||||
("protected", declaration.Parser),
|
||||
("noncomputable", declaration.Parser),
|
||||
("unsafe", declaration.Parser),
|
||||
("def", declaration.Parser),
|
||||
("abbreviation", declaration.Parser),
|
||||
("abbrev", declaration.Parser),
|
||||
("theorem", declaration.Parser),
|
||||
("instance", declaration.Parser),
|
||||
("axiom", declaration.Parser),
|
||||
("constant", declaration.Parser),
|
||||
("class", declaration.Parser),
|
||||
("inductive", declaration.Parser),
|
||||
("structure", declaration.Parser),
|
||||
|
||||
("variable", variable.Parser),
|
||||
("variables", variables.Parser),
|
||||
("namespace", namespace.Parser),
|
||||
("end", end.Parser),
|
||||
("open", open.Parser),
|
||||
("section", section.Parser),
|
||||
("universe", universe.Parser),
|
||||
("universes", universe.Parser),
|
||||
("local", notation.Parser),
|
||||
("notation", notation.Parser),
|
||||
("reserve", reserveNotation.Parser),
|
||||
("local", mixfix.Parser),
|
||||
("prefix", mixfix.Parser),
|
||||
("infix", mixfix.Parser),
|
||||
("infixl", mixfix.Parser),
|
||||
("infixr", mixfix.Parser),
|
||||
("postfix", mixfix.Parser),
|
||||
("reserve", reserveMixfix.Parser),
|
||||
("#check", check.Parser),
|
||||
("local", attribute.Parser),
|
||||
("attribute", attribute.Parser),
|
||||
("export", export.Parser),
|
||||
("include", include.Parser),
|
||||
("omit", omit.Parser),
|
||||
("initQuot", initQuot.Parser),
|
||||
("setOption", setOption.Parser)]
|
||||
end «command»
|
||||
|
||||
def commandParser.run (commands : TokenMap commandParser) (p : commandParser)
|
||||
: ParserT CommandParserConfig Id Syntax :=
|
||||
λ cfg, (p.run cfg).runParsec $ λ _, (indexed commands >>= anyOf : commandParser).run cfg
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,167 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Parsers for commands that declare things
|
||||
-/
|
||||
|
||||
prelude
|
||||
import init.lean.parser.term
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
open Combinators MonadParsec
|
||||
open Parser.HasTokens Parser.HasView
|
||||
|
||||
instance termParserCommandParserCoe : HasCoe termParser commandParser :=
|
||||
⟨λ p, adaptReader coe $ p.run⟩
|
||||
|
||||
namespace «command»
|
||||
|
||||
local postfix `?`:10000 := optional
|
||||
local postfix *:10000 := Combinators.many
|
||||
local postfix +:10000 := Combinators.many1
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def docComment.Parser : commandParser :=
|
||||
node! docComment ["/--", doc: raw $ many' (notFollowedBy (str "-/") *> any), "-/"]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def attrInstance.Parser : commandParser :=
|
||||
-- use `rawIdent` because of attribute names such as `instance`
|
||||
node! attrInstance [Name: rawIdent.Parser, args: (Term.Parser maxPrec)*]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def declAttributes.Parser : commandParser :=
|
||||
-- TODO(Sebastian): custom attribute parsers
|
||||
node! declAttributes ["@[", attrs: sepBy1 attrInstance.Parser (symbol ","), "]"]
|
||||
|
||||
set_option class.instance_max_depth 300
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def declModifiers.Parser : commandParser :=
|
||||
node! declModifiers [
|
||||
docComment: docComment.Parser?,
|
||||
attrs: declAttributes.Parser?,
|
||||
visibility: nodeChoice! visibility {"private", "protected"}?,
|
||||
«noncomputable»: (symbol "noncomputable")?,
|
||||
«unsafe»: (symbol "unsafe")?,
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def declSig.Parser : commandParser :=
|
||||
node! declSig [
|
||||
params: Term.bracketedBinders.Parser,
|
||||
type: Term.typeSpec.Parser,
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def optDeclSig.Parser : commandParser :=
|
||||
node! optDeclSig [
|
||||
params: Term.bracketedBinders.Parser,
|
||||
type: Term.optType.Parser,
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def equation.Parser : commandParser :=
|
||||
node! equation ["|", lhs: (Term.Parser maxPrec)+, ":=", rhs: Term.Parser]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def declVal.Parser : commandParser :=
|
||||
nodeChoice! declVal {
|
||||
simple: node! simpleDeclVal [":=", body: Term.Parser],
|
||||
emptyMatch: symbol ".",
|
||||
«match»: equation.Parser+
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def inferModifier.Parser : commandParser :=
|
||||
nodeChoice! inferModifier {
|
||||
relaxed: try $ node! relaxedInferModifier ["{", "}"],
|
||||
strict: try $ node! strictInferModifier ["(", ")"],
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def introRule.Parser : commandParser :=
|
||||
node! introRule [
|
||||
"|",
|
||||
Name: ident.Parser,
|
||||
inferMod: inferModifier.Parser?,
|
||||
sig: optDeclSig.Parser,
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def structBinderContent.Parser : commandParser :=
|
||||
node! structBinderContent [
|
||||
ids: ident.Parser+,
|
||||
inferMod: inferModifier.Parser?,
|
||||
sig: optDeclSig.Parser,
|
||||
default: Term.binderDefault.Parser?,
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def structureFieldBlock.Parser : commandParser :=
|
||||
nodeChoice! structureFieldBlock {
|
||||
explicit: node! structExplicitBinder ["(", content: nodeChoice! structExplicitBinderContent {
|
||||
«notation»: command.notationLike.Parser,
|
||||
other: structBinderContent.Parser
|
||||
}, right: symbol ")"],
|
||||
implicit: node! structImplicitBinder ["{", content: structBinderContent.Parser, "}"],
|
||||
strictImplicit: node! strictImplicitBinder ["⦃", content: structBinderContent.Parser, "⦄"],
|
||||
instImplicit: node! instImplicitBinder ["[", content: structBinderContent.Parser, "]"],
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def oldUnivParams.Parser : commandParser :=
|
||||
node! oldUnivParams ["{", ids: ident.Parser+, "}"]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def identUnivParams.Parser : commandParser :=
|
||||
node! identUnivParams [
|
||||
id: ident.Parser,
|
||||
univParams: node! univParams [".{", params: ident.Parser+, "}"]?
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def structure.Parser : commandParser :=
|
||||
node! «structure» [
|
||||
keyword: nodeChoice! structureKw {"structure", "class"},
|
||||
oldUnivParams: oldUnivParams.Parser?,
|
||||
Name: identUnivParams.Parser,
|
||||
sig: optDeclSig.Parser,
|
||||
«extends»: node! «extends» ["extends", parents: sepBy1 Term.Parser (symbol ",")]?,
|
||||
":=",
|
||||
ctor: node! structureCtor [Name: ident.Parser, inferMod: inferModifier.Parser?, "::"]?,
|
||||
fieldBlocks: structureFieldBlock.Parser*,
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def declaration.Parser : commandParser :=
|
||||
node! declaration [
|
||||
modifiers: declModifiers.Parser,
|
||||
inner: nodeChoice! declaration.inner {
|
||||
«defLike»: node! «defLike» [
|
||||
kind: nodeChoice! defLike.kind {"def", "abbreviation", "abbrev", "theorem", "constant"},
|
||||
oldUnivParams: oldUnivParams.Parser?,
|
||||
Name: identUnivParams.Parser, sig: optDeclSig.Parser, val: declVal.Parser],
|
||||
«instance»: node! «instance» ["instance", Name: identUnivParams.Parser?, sig: declSig.Parser, val: declVal.Parser],
|
||||
«example»: node! «example» ["example", sig: declSig.Parser, val: declVal.Parser],
|
||||
«axiom»: node! «axiom» [
|
||||
kw: nodeChoice! constantKeyword {"axiom"},
|
||||
Name: identUnivParams.Parser,
|
||||
sig: declSig.Parser],
|
||||
«inductive»: node! «inductive» [try [«class»: (symbol "class")?, "inductive"],
|
||||
oldUnivParams: oldUnivParams.Parser?,
|
||||
Name: identUnivParams.Parser,
|
||||
sig: optDeclSig.Parser,
|
||||
localNotation: notationLike.Parser?,
|
||||
introRules: introRule.Parser*],
|
||||
«structure»: structure.Parser,
|
||||
}
|
||||
]
|
||||
|
||||
end «command»
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.data.char.basic init.lean.parser.parsec
|
||||
|
||||
namespace Lean
|
||||
|
||||
def isGreek (c : Char) : Bool :=
|
||||
0x391 ≤ c.val && c.val ≤ 0x3dd
|
||||
|
||||
def isLetterLike (c : Char) : Bool :=
|
||||
(0x3b1 ≤ c.val && c.val ≤ 0x3c9 && c.val ≠ 0x3bb) || -- Lower greek, but lambda
|
||||
(0x391 ≤ c.val && c.val ≤ 0x3A9 && c.val ≠ 0x3A0 && c.val ≠ 0x3A3) || -- Upper greek, but Pi and Sigma
|
||||
(0x3ca ≤ c.val && c.val ≤ 0x3fb) || -- Coptic letters
|
||||
(0x1f00 ≤ c.val && c.val ≤ 0x1ffe) || -- Polytonic Greek Extended Character Set
|
||||
(0x2100 ≤ c.val && c.val ≤ 0x214f) || -- Letter like block
|
||||
(0x1d49c ≤ c.val && c.val ≤ 0x1d59f) -- Latin letters, Script, Double-struck, Fractur
|
||||
|
||||
def isSubScriptAlnum (c : Char) : Bool :=
|
||||
(0x207f ≤ c.val && c.val ≤ 0x2089) || -- n superscript and numberic subscripts
|
||||
(0x2090 ≤ c.val && c.val ≤ 0x209c) ||
|
||||
(0x1d62 ≤ c.val && c.val ≤ 0x1d6a)
|
||||
|
||||
def isIdFirst (c : Char) : Bool :=
|
||||
c.isAlpha || c = '_' || isLetterLike c
|
||||
|
||||
def isIdRest (c : Char) : Bool :=
|
||||
c.isAlphanum || c = '_' || c = '\'' || isLetterLike c || isSubScriptAlnum c
|
||||
|
||||
def idBeginEscape := '«'
|
||||
def idEndEscape := '»'
|
||||
def isIdBeginEscape (c : Char) : Bool :=
|
||||
c = idBeginEscape
|
||||
def isIdEndEscape (c : Char) : Bool :=
|
||||
c = idEndEscape
|
||||
|
||||
namespace Parser
|
||||
variables {m : Type → Type} {μ : Type} [Monad m] [MonadParsec μ m] [Alternative m]
|
||||
open MonadParsec
|
||||
|
||||
def idPartDefault : m String :=
|
||||
do c ← satisfy isIdFirst,
|
||||
takeWhileCont isIdRest (toString c)
|
||||
|
||||
def idPartEscaped : m String :=
|
||||
ch idBeginEscape *> takeUntil1 isIdEndEscape <* ch idEndEscape
|
||||
|
||||
def idPart : m String :=
|
||||
cond isIdBeginEscape
|
||||
idPartEscaped
|
||||
idPartDefault
|
||||
|
||||
def identifier : m Name :=
|
||||
(try $ do s ← idPart,
|
||||
foldl Name.mkString (mkSimpleName s) (ch '.' *> idPart)) <?> "identifier"
|
||||
|
||||
def cIdentifier : m String :=
|
||||
(try $ do c ← satisfy (λ c, c.isAlpha || c = '_'),
|
||||
takeWhileCont (λ c, c.isAlphanum || c = '_') (toString c)) <?> "C identifier"
|
||||
|
||||
def cppIdentifier : m String :=
|
||||
(try $ do n ← cIdentifier,
|
||||
ns ← many ((++) <$> str "::" <*> cIdentifier),
|
||||
pure $ String.join (n::ns)) <?> "C++ identifier"
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,76 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Level-Level parsers
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.pratt
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
open Combinators Parser.HasView MonadParsec
|
||||
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept MonadRec monadBasicParser]
|
||||
def LevelParserM := RecT Nat Syntax BasicParserM
|
||||
abbrev levelParser := LevelParserM Syntax
|
||||
|
||||
/-- A Level Parser for a suffix or infix notation that accepts a preceding Term Level. -/
|
||||
@[derive Monad Alternative MonadReader MonadParsec MonadExcept MonadRec monadBasicParser]
|
||||
def TrailingLevelParserM := ReaderT Syntax LevelParserM
|
||||
abbrev trailingLevelParser := TrailingLevelParserM Syntax
|
||||
|
||||
instance trailingLevelParserCoe : HasCoe levelParser trailingLevelParser :=
|
||||
⟨λ x _, x⟩
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def Level.Parser (rbp := 0) : levelParser :=
|
||||
recurse rbp <?> "universe Level"
|
||||
|
||||
namespace Level
|
||||
/-- Access leading Term -/
|
||||
def getLeading : trailingLevelParser := read
|
||||
instance : HasTokens getLeading := default _
|
||||
instance : HasView Syntax getLeading := default _
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def paren.Parser : levelParser :=
|
||||
node! «paren» ["(":maxPrec, inner: Level.Parser 0, ")"]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def leading.Parser : levelParser :=
|
||||
nodeChoice! leading {
|
||||
max: symbolOrIdent "max",
|
||||
imax: symbolOrIdent "imax",
|
||||
hole: symbol "_" maxPrec,
|
||||
paren: paren.Parser,
|
||||
lit: number.Parser,
|
||||
var: ident.Parser
|
||||
}
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def app.Parser : trailingLevelParser :=
|
||||
node! app [fn: getLeading, Arg: Level.Parser maxPrec]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def addLit.Parser : trailingLevelParser :=
|
||||
node! addLit [lhs: getLeading, "+", rhs: number.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def trailing.Parser : trailingLevelParser :=
|
||||
nodeChoice! trailing {
|
||||
app: app.Parser,
|
||||
addLit: addLit.Parser
|
||||
}
|
||||
end Level
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def levelParser.run (p : levelParser) : basicParser :=
|
||||
prattParser Level.leading.Parser Level.trailing.Parser p
|
||||
|
||||
instance levelParserCoe : HasCoe levelParser basicParser :=
|
||||
⟨levelParser.run⟩
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,133 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Module-Level parsers
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.command
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
open Combinators MonadParsec
|
||||
open Parser.HasTokens Parser.HasView
|
||||
|
||||
local postfix `?`:10000 := optional
|
||||
local postfix *:10000 := Combinators.many
|
||||
local postfix +:10000 := Combinators.many1
|
||||
|
||||
structure ModuleParserConfig extends CommandParserConfig :=
|
||||
(commandParsers : TokenMap commandParser)
|
||||
|
||||
instance moduleParserConfigCoe : HasCoe ModuleParserConfig CommandParserConfig :=
|
||||
⟨ModuleParserConfig.toCommandParserConfig⟩
|
||||
|
||||
section
|
||||
@[derive Monad Alternative MonadReader MonadState MonadParsec MonadExcept]
|
||||
def ModuleParserM := StateT ParserState $ ParserT ModuleParserConfig Id
|
||||
abbrev moduleParser := ModuleParserM Syntax
|
||||
end
|
||||
|
||||
instance ModuleParserM.liftParserT (ρ : Type) [HasLiftT ModuleParserConfig ρ] :
|
||||
HasMonadLift (ParserT ρ Id) ModuleParserM :=
|
||||
{ monadLift := λ α x st cfg, (λ a, (a, st)) <$> x.run ↑cfg }
|
||||
|
||||
section
|
||||
local attribute [reducible] BasicParserM
|
||||
instance ModuleParserM.BasicParserM (ρ : Type) [HasLiftT ModuleParserConfig ρ] :
|
||||
HasMonadLift BasicParserM ModuleParserM :=
|
||||
inferInstance
|
||||
end
|
||||
|
||||
namespace Module
|
||||
@[derive Parser.HasView Parser.HasTokens]
|
||||
def prelude.Parser : basicParser :=
|
||||
node! «prelude» ["prelude"]
|
||||
|
||||
@[derive Parser.HasView Parser.HasTokens]
|
||||
def importPath.Parser : basicParser :=
|
||||
-- use `raw` to ignore registered tokens like ".."
|
||||
node! importPath [
|
||||
dirups: (rawStr ".")*,
|
||||
Module: ident.Parser]
|
||||
|
||||
@[derive Parser.HasView Parser.HasTokens]
|
||||
def import.Parser : basicParser :=
|
||||
node! «import» ["import", imports: importPath.Parser+]
|
||||
|
||||
@[derive Parser.HasView Parser.HasTokens]
|
||||
def header.Parser : basicParser :=
|
||||
node! «header» [«prelude»: prelude.Parser?, imports: import.Parser*]
|
||||
|
||||
@[pattern] def eoi : SyntaxNodeKind := ⟨`Lean.Parser.Module.eoi⟩
|
||||
|
||||
def eoi.Parser : moduleParser := do
|
||||
MonadParsec.eoi,
|
||||
it ← leftOver,
|
||||
-- add `eoi` Node for left-over input
|
||||
let stop := it.toEnd,
|
||||
pure $ Syntax.mkNode eoi [Syntax.atom ⟨some ⟨⟨stop, stop⟩, stop.offset, ⟨stop, stop⟩⟩, ""⟩]
|
||||
|
||||
/-- Read command, recovering from errors inside commands (attach partial Syntax tree)
|
||||
as well as unknown commands (skip input). -/
|
||||
private def commandWrecAux : Bool → Nat → ModuleParserM (Bool × Syntax)
|
||||
| recovering 0 := error "unreachable"
|
||||
| recovering (Nat.succ n) := do
|
||||
-- terminate at EOF
|
||||
Nat.succ _ ← remaining | (Prod.mk false) <$> eoi.Parser,
|
||||
(recovering, c) ← catch (do {
|
||||
cfg ← read,
|
||||
c ← monadLift $ command.Parser.run cfg.commandParsers,
|
||||
pure (false, some c)
|
||||
} <|> do {
|
||||
-- unknown command: try to skip token, or else single character
|
||||
when (¬ recovering) $ do {
|
||||
it ← leftOver,
|
||||
logMessage {expected := DList.singleton "command", it := it, custom := some ()}
|
||||
},
|
||||
try (monadLift token *> pure ()) <|> (any *> pure ()),
|
||||
pure (true, none)
|
||||
}) $ λ msg, do {
|
||||
-- error inside command: log error, return partial Syntax tree
|
||||
logMessage msg,
|
||||
pure (true, some msg.custom.get)
|
||||
},
|
||||
/- NOTE: We need to make very sure that these recursive calls are happening in tail positions.
|
||||
Otherwise, resuming the coroutine is linear in the number of previous commands. -/
|
||||
match c with
|
||||
| some c := pure (recovering, c)
|
||||
| none := commandWrecAux recovering n
|
||||
|
||||
def parseCommandWithRecovery (recovering : Bool) :=
|
||||
do { rem ← remaining, commandWrecAux recovering rem.succ }
|
||||
end Module
|
||||
open Module
|
||||
|
||||
structure ModuleParserSnapshot :=
|
||||
-- it there was a parse error in the previous command, we shouldn't complain if parsing immediately after it
|
||||
-- fails as well
|
||||
(recovering : Bool)
|
||||
(it : String.OldIterator)
|
||||
|
||||
-- return (partial) Syntax tree and single fatal or multiple non-fatal messages
|
||||
def resumeModuleParser {α : Type} (cfg : ModuleParserConfig) (snap : ModuleParserSnapshot) (mkRes : α → Syntax × ModuleParserSnapshot)
|
||||
(p : ModuleParserM α) : Syntax × Except Message (ModuleParserSnapshot × MessageLog) :=
|
||||
let (r, _) := ((((Prod.mk <$> p <*> leftOver).run {messages:=MessageLog.empty}).run cfg).runFrom snap.it).run {} in
|
||||
match r with
|
||||
| Except.ok ((a, it), st) := let (stx, snap) := mkRes a in (stx, Except.ok ({snap with it := it}, st.messages))
|
||||
| Except.error msg := (msg.custom.get, Except.error $ messageOfParsecMessage cfg msg)
|
||||
|
||||
def parseHeader (cfg : ModuleParserConfig) :=
|
||||
let snap := {ModuleParserSnapshot . recovering := false, it := cfg.input.mkOldIterator} in
|
||||
resumeModuleParser cfg snap (λ stx, (stx, snap)) $ do
|
||||
-- `token` assumes that there is no leading whitespace
|
||||
monadLift whitespace,
|
||||
monadLift header.Parser
|
||||
|
||||
def parseCommand (cfg) (snap) := resumeModuleParser cfg snap (λ p, (Prod.snd p, {snap with recovering := Prod.fst p}))
|
||||
(parseCommandWithRecovery snap.recovering)
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,189 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Notation parsers
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.token
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
open Combinators MonadParsec
|
||||
open Parser.HasTokens Parser.HasView
|
||||
|
||||
local postfix `?`:10000 := optional
|
||||
local postfix *:10000 := Combinators.many
|
||||
local postfix +:10000 := Combinators.many1
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def Term.Parser (rbp := 0) : termParser :=
|
||||
recurse rbp <?> "Term"
|
||||
|
||||
set_option class.instance_max_depth 100
|
||||
|
||||
namespace «command»
|
||||
namespace NotationSpec
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def precedenceLit.Parser : termParser :=
|
||||
nodeChoice! precedenceLit {
|
||||
num: number.Parser,
|
||||
max: symbolOrIdent "max",
|
||||
-- TODO(Sebastian): `precOf`?
|
||||
}
|
||||
|
||||
def precedenceLit.View.toNat : precedenceLit.View → Nat
|
||||
| (precedenceLit.View.num n) := n.toNat
|
||||
| (precedenceLit.View.max _) := maxPrec
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def precedenceTerm.Parser : termParser :=
|
||||
nodeChoice! precedenceTerm {
|
||||
lit: precedenceLit.Parser,
|
||||
offset: node! precedenceOffset ["(", lit: precedenceLit.Parser,
|
||||
op: nodeChoice! precedenceOffsetOp {" + ", " - "},
|
||||
offset: number.Parser,
|
||||
")",
|
||||
]
|
||||
}
|
||||
|
||||
def precedenceTerm.View.toNat : precedenceTerm.View → Nat
|
||||
| (precedenceTerm.View.lit l) := l.toNat
|
||||
| (precedenceTerm.View.offset o) := match o.op with
|
||||
| (precedenceOffsetOp.View.«+» _) := o.lit.toNat.add o.offset.toNat
|
||||
| (precedenceOffsetOp.View.«-» _) := o.lit.toNat - o.offset.toNat
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def precedence.Parser : termParser :=
|
||||
node! «precedence» [":", Term: precedenceTerm.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def quotedSymbol.Parser : termParser :=
|
||||
raw $ takeUntil (= '`')
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def symbolQuote.Parser : termParser :=
|
||||
node! symbolQuote [
|
||||
leftQuote: rawStr "`",
|
||||
symbol: quotedSymbol.Parser,
|
||||
rightQuote: rawStr "`" true, -- consume trailing ws
|
||||
prec: precedence.Parser?]
|
||||
|
||||
def unquotedSymbol.Parser : termParser :=
|
||||
try $ do {
|
||||
it ← leftOver,
|
||||
stx@(Syntax.atom _) ← monadLift token | error "" (DList.singleton "symbol") it,
|
||||
pure stx
|
||||
} <?> "symbol"
|
||||
|
||||
instance unquotedSymbol.tokens : Parser.HasTokens unquotedSymbol.Parser := ⟨[]⟩
|
||||
instance unquotedSymbol.View : Parser.HasView (Option SyntaxAtom) unquotedSymbol.Parser :=
|
||||
{ view := λ stx, match stx with
|
||||
| Syntax.atom atom := some atom
|
||||
| _ := none,
|
||||
review := λ a, (Syntax.atom <$> a).getOrElse Syntax.missing }
|
||||
|
||||
--TODO(Sebastian): cannot be called `symbol` because of hygiene problems
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def notationSymbol.Parser : termParser :=
|
||||
nodeChoice! notationSymbol {
|
||||
quoted: symbolQuote.Parser,
|
||||
--TODO(Sebastian): decide if we want this in notations
|
||||
--unquoted: unquotedSymbol.Parser
|
||||
}
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def mixfixSymbol.Parser : termParser :=
|
||||
nodeChoice! mixfixSymbol {
|
||||
quoted: symbolQuote.Parser,
|
||||
unquoted: unquotedSymbol.Parser
|
||||
}
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def foldAction.Parser : termParser :=
|
||||
node! foldAction [
|
||||
"(",
|
||||
op: anyOf [symbolOrIdent "foldl", symbolOrIdent "foldr"],
|
||||
sep: notationSymbol.Parser,
|
||||
folder: node! foldActionFolder [
|
||||
"(",
|
||||
arg1: ident.Parser,
|
||||
arg2: ident.Parser,
|
||||
",",
|
||||
rhs: Term.Parser,
|
||||
")"
|
||||
],
|
||||
init: Term.Parser,
|
||||
endTk: notationSymbol.Parser,
|
||||
")"
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def action.Parser : termParser :=
|
||||
node! action [":", kind: nodeChoice! actionKind {
|
||||
prec: try precedenceTerm.Parser,
|
||||
prev: symbolOrIdent "prev",
|
||||
scoped: node! scopedAction [
|
||||
try ["(", scoped: symbolOrIdent "scoped"],
|
||||
prec: precedence.Parser?,
|
||||
id: ident.Parser,
|
||||
", ",
|
||||
Term: Term.Parser,
|
||||
")",
|
||||
],
|
||||
fold: foldAction.Parser
|
||||
}]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def transition.Parser : termParser :=
|
||||
nodeChoice! transition {
|
||||
binder: node! binder [binder: symbolOrIdent "binder", prec: precedence.Parser?],
|
||||
binders: node! binders [binders: symbolOrIdent "binders", prec: precedence.Parser?],
|
||||
Arg: node! argument [id: ident.Parser, action: action.Parser?]
|
||||
}
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def rule.Parser : termParser :=
|
||||
node! rule [symbol: notationSymbol.Parser, transition: transition.Parser?]
|
||||
|
||||
end NotationSpec
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def NotationSpec.Parser : termParser :=
|
||||
node! NotationSpec [prefixArg: ident.Parser?, rules: NotationSpec.rule.Parser*]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def notation.Parser : termParser :=
|
||||
node! «notation» [
|
||||
try [«local»: (symbol "local ")?, "notation"],
|
||||
spec: NotationSpec.Parser, ":=", Term: Term.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def reserveNotation.Parser : termParser :=
|
||||
node! «reserveNotation» [try ["reserve", "notation"], spec: NotationSpec.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def mixfix.kind.Parser : termParser :=
|
||||
nodeChoice! mixfix.kind {"prefix", "infix", "infixl", "infixr", "postfix"}
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def mixfix.Parser : termParser :=
|
||||
node! «mixfix» [
|
||||
try [«local»: (symbol "local ")?, kind: mixfix.kind.Parser],
|
||||
symbol: NotationSpec.mixfixSymbol.Parser, ":=", Term: Term.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def notationLike.Parser : termParser :=
|
||||
nodeChoice! notationLike {«notation»: notation.Parser, mixfix: mixfix.Parser}
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def reserveMixfix.Parser : termParser :=
|
||||
node! «reserveMixfix» [
|
||||
try ["reserve", kind: mixfix.kind.Parser],
|
||||
symbol: NotationSpec.notationSymbol.Parser]
|
||||
|
||||
end «command»
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,674 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura, Sebastian Ullrich
|
||||
|
||||
Implementation for the Parsec Parser Combinators described in the
|
||||
paper:
|
||||
https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/Parsec-paper-letter.pdf
|
||||
-/
|
||||
prelude
|
||||
import init.data.tostring init.data.string.basic init.data.list.basic init.control.except
|
||||
import init.data.repr init.lean.name init.data.dlist init.control.monadfail init.control.combinators
|
||||
import init.lean.format
|
||||
|
||||
/- Old String iterator -/
|
||||
namespace String
|
||||
structure OldIterator :=
|
||||
(s : String) (offset : Nat) (i : Nat)
|
||||
|
||||
def mkOldIterator (s : String) : OldIterator :=
|
||||
⟨s, 0, 0⟩
|
||||
|
||||
namespace OldIterator
|
||||
def remaining : OldIterator → Nat
|
||||
| ⟨s, o, _⟩ := s.length - o
|
||||
|
||||
def toString : OldIterator → String
|
||||
| ⟨s, _, _⟩ := s
|
||||
|
||||
def remainingBytes : OldIterator → Nat
|
||||
| ⟨s, _, i⟩ := s.bsize - i
|
||||
|
||||
def curr : OldIterator → Char
|
||||
| ⟨s, _, i⟩ := get s i
|
||||
|
||||
def next : OldIterator → OldIterator
|
||||
| ⟨s, o, i⟩ := ⟨s, o+1, s.next i⟩
|
||||
|
||||
def prev : OldIterator → OldIterator
|
||||
| ⟨s, o, i⟩ := ⟨s, o-1, s.prev i⟩
|
||||
|
||||
def hasNext : OldIterator → Bool
|
||||
| ⟨s, _, i⟩ := i < utf8ByteSize s
|
||||
|
||||
def hasPrev : OldIterator → Bool
|
||||
| ⟨s, _, i⟩ := i > 0
|
||||
|
||||
def setCurr : OldIterator → Char → OldIterator
|
||||
| ⟨s, o, i⟩ c := ⟨s.set i c, o, i⟩
|
||||
|
||||
def toEnd : OldIterator → OldIterator
|
||||
| ⟨s, o, _⟩ := ⟨s, s.length, s.bsize⟩
|
||||
|
||||
def extract : OldIterator → OldIterator → String
|
||||
| ⟨s₁, _, b⟩ ⟨s₂, _, e⟩ :=
|
||||
if s₁ ≠ s₂ || b > e then ""
|
||||
else s₁.extract b e
|
||||
|
||||
def forward : OldIterator → Nat → OldIterator
|
||||
| it 0 := it
|
||||
| it (n+1) := forward it.next n
|
||||
|
||||
def remainingToString : OldIterator → String
|
||||
| ⟨s, _, i⟩ := s.extract i s.bsize
|
||||
|
||||
/- (isPrefixOfRemaining it₁ it₂) is `true` Iff `it₁.remainingToString` is a prefix
|
||||
of `it₂.remainingToString`. -/
|
||||
def isPrefixOfRemaining : OldIterator → OldIterator → Bool
|
||||
| ⟨s₁, _, i₁⟩ ⟨s₂, _, i₂⟩ := s₁.extract i₁ s₁.bsize = s₂.extract i₂ (i₂ + (s₁.bsize - i₁))
|
||||
|
||||
def nextn : OldIterator → Nat → OldIterator
|
||||
| it 0 := it
|
||||
| it (i+1) := nextn it.next i
|
||||
|
||||
def prevn : OldIterator → Nat → OldIterator
|
||||
| it 0 := it
|
||||
| it (i+1) := prevn it.prev i
|
||||
end OldIterator
|
||||
|
||||
private def oldLineColumnAux : Nat → String.OldIterator → Nat × Nat → Nat × Nat
|
||||
| 0 it r := r
|
||||
| (k+1) it r@(line, col) :=
|
||||
if it.hasNext = false then r
|
||||
else match it.curr with
|
||||
| '\n' := oldLineColumnAux k it.next (line+1, 0)
|
||||
| other := oldLineColumnAux k it.next (line, col+1)
|
||||
|
||||
def oldLineColumn (s : String) (offset : Nat) : Nat × Nat :=
|
||||
oldLineColumnAux offset s.mkOldIterator (1, 0)
|
||||
|
||||
end String
|
||||
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
open String (OldIterator)
|
||||
|
||||
namespace Parsec
|
||||
@[reducible] def Position : Type := Nat
|
||||
|
||||
structure Message (μ : Type := Unit) :=
|
||||
(it : OldIterator)
|
||||
(unexpected : String := "") -- unexpected input
|
||||
(expected : DList String := ∅) -- expected productions
|
||||
(custom : Option μ)
|
||||
|
||||
def expected.toString : List String → String
|
||||
| [] := ""
|
||||
| [e] := e
|
||||
| [e1, e2] := e1 ++ " or " ++ e2
|
||||
| (e::es) := e ++ ", " ++ expected.toString es
|
||||
|
||||
def Message.text {μ : Type} (msg : Message μ) : String :=
|
||||
let unexpected := (if msg.unexpected = "" then [] else ["unexpected " ++ msg.unexpected]) in
|
||||
let exList := msg.expected.toList in
|
||||
let expected := if exList = [] then [] else ["expected " ++ expected.toString exList] in
|
||||
"\n".intercalate $ unexpected ++ expected
|
||||
|
||||
|
||||
protected def Message.toString {μ : Type} (msg : Message μ) : String :=
|
||||
let (line, col) := msg.it.toString.oldLineColumn msg.it.offset in
|
||||
-- always print ":"; we assume at least one of `unexpected` and `expected` to be non-Empty
|
||||
"error at line " ++ toString line ++ ", column " ++ toString col ++ ":\n" ++ msg.text
|
||||
|
||||
instance {μ : Type} : HasToString (Message μ) :=
|
||||
⟨Message.toString⟩
|
||||
|
||||
-- use for e.g. upcasting Parsec errors with `MonadExcept.liftExcept`
|
||||
instance {μ : Type} : HasLift (Message μ) String :=
|
||||
⟨toString⟩
|
||||
|
||||
/-
|
||||
Remark: we store expected "error" messages in `okEps` results.
|
||||
They contain the error that would have occurred if a
|
||||
successful "epsilon" Alternative was not taken.
|
||||
-/
|
||||
inductive Result (μ α : Type)
|
||||
| ok {} (a : α) (it : OldIterator) (expected : Option $ DList String) : Result
|
||||
| error {} (msg : Message μ) (consumed : Bool) : Result
|
||||
|
||||
@[inline] def Result.mkEps {μ α : Type} (a : α) (it : OldIterator) : Result μ α :=
|
||||
Result.ok a it (some ∅)
|
||||
end Parsec
|
||||
|
||||
open Parsec
|
||||
|
||||
def ParsecT (μ : Type) (m : Type → Type) (α : Type) :=
|
||||
OldIterator → m (Result μ α)
|
||||
|
||||
abbrev Parsec (μ : Type) := ParsecT μ Id
|
||||
/-- `Parsec` without custom error Message Type -/
|
||||
abbrev Parsec' := Parsec Unit
|
||||
|
||||
namespace ParsecT
|
||||
open Parsec.Result
|
||||
variables {m : Type → Type} [Monad m] {μ α β : Type}
|
||||
|
||||
def run (p : ParsecT μ m α) (s : String) (fname := "") : m (Except (Message μ) α) :=
|
||||
do r ← p s.mkOldIterator,
|
||||
pure $ match r with
|
||||
| ok a _ _ := Except.ok a
|
||||
| error msg _ := Except.error msg
|
||||
|
||||
def runFrom (p : ParsecT μ m α) (it : OldIterator) (fname := "") : m (Except (Message μ) α) :=
|
||||
do r ← p it,
|
||||
pure $ match r with
|
||||
| ok a _ _ := Except.ok a
|
||||
| error msg _ := Except.error msg
|
||||
|
||||
@[inline] protected def pure (a : α) : ParsecT μ m α :=
|
||||
λ it, pure (mkEps a it)
|
||||
|
||||
def eps : ParsecT μ m Unit :=
|
||||
ParsecT.pure ()
|
||||
|
||||
protected def failure : ParsecT μ m α :=
|
||||
λ it, pure (error { unexpected := "failure", it := it, custom := none } false)
|
||||
|
||||
def merge (msg₁ msg₂ : Message μ) : Message μ :=
|
||||
{ expected := msg₁.expected ++ msg₂.expected, ..msg₁ }
|
||||
|
||||
@[inlineIfReduce] def bindMkRes (ex₁ : Option (DList String)) (r : Result μ β) : Result μ β :=
|
||||
match ex₁, r with
|
||||
| none, ok b it _ := ok b it none
|
||||
| none, error msg _ := error msg true
|
||||
| some ex₁, ok b it (some ex₂) := ok b it (some $ ex₁ ++ ex₂)
|
||||
| some ex₁, error msg₂ false := error { expected := ex₁ ++ msg₂.expected, .. msg₂ } false
|
||||
| some ex₁, other := other
|
||||
|
||||
/--
|
||||
The `bind p q` Combinator behaves as follows:
|
||||
1- If `p` fails, then it fails.
|
||||
2- If `p` succeeds and consumes input, then execute `q`
|
||||
3- If `q` succeeds but does not consume input, then execute `q`
|
||||
and merge error messages if both do not consume any input.
|
||||
-/
|
||||
@[inline] protected def bind (p : ParsecT μ m α) (q : α → ParsecT μ m β) : ParsecT μ m β :=
|
||||
λ it, do
|
||||
r ← p it,
|
||||
match r with
|
||||
| ok a it ex₁ := bindMkRes ex₁ <$> q a it
|
||||
| error msg c := pure (error msg c)
|
||||
|
||||
/-- More efficient `bind` that does not correctly merge `expected` and `consumed` information. -/
|
||||
@[inline] def bind' (p : ParsecT μ m α) (q : α → ParsecT μ m β) : ParsecT μ m β :=
|
||||
λ it, do
|
||||
r ← p it,
|
||||
match r with
|
||||
| ok a it ex₁ := q a it
|
||||
| error msg c := pure (error msg c)
|
||||
|
||||
instance : Monad (ParsecT μ m) :=
|
||||
{ bind := λ _ _, ParsecT.bind, pure := λ _, ParsecT.pure }
|
||||
|
||||
/-- `Monad` instance using `bind'`. -/
|
||||
def Monad' : Monad (ParsecT μ m) :=
|
||||
{ bind := λ _ _, ParsecT.bind', pure := λ _, ParsecT.pure }
|
||||
|
||||
instance : MonadFail Parsec' :=
|
||||
{ fail := λ _ s it, error { unexpected := s, it := it, custom := () } false }
|
||||
|
||||
instance : MonadExcept (Message μ) (ParsecT μ m) :=
|
||||
{ throw := λ _ msg it, pure (error msg false),
|
||||
catch := λ _ p c it, do
|
||||
r ← p it,
|
||||
match r with
|
||||
| error msg cns := do {
|
||||
r ← c msg msg.it,
|
||||
pure $ match r with
|
||||
| error msg' cns' := error msg' (cns || cns')
|
||||
| other := other }
|
||||
| other := pure other }
|
||||
|
||||
instance : HasMonadLift m (ParsecT μ m) :=
|
||||
{ monadLift := λ α x it, do a ← x, pure (mkEps a it) }
|
||||
|
||||
def expect (msg : Message μ) (exp : String) : Message μ :=
|
||||
{expected := DList.singleton exp, ..msg}
|
||||
|
||||
@[inlineIfReduce] def labelsMkRes (r : Result μ α) (lbls : DList String) : Result μ α :=
|
||||
match r with
|
||||
| ok a it (some _) := ok a it (some lbls)
|
||||
| error msg false := error {expected := lbls, ..msg} false
|
||||
| other := other
|
||||
|
||||
@[inline] def labels (p : ParsecT μ m α) (lbls : DList String) : ParsecT μ m α :=
|
||||
λ it, do
|
||||
r ← p it,
|
||||
pure $ labelsMkRes r lbls
|
||||
|
||||
@[inlineIfReduce] def tryMkRes (r : Result μ α) : Result μ α :=
|
||||
match r with
|
||||
| error msg _ := error msg false
|
||||
| other := other
|
||||
|
||||
/--
|
||||
`try p` behaves like `p`, but it pretends `p` hasn't
|
||||
consumed any input when `p` fails.
|
||||
|
||||
It is useful for implementing infinite lookahead.
|
||||
The Parser `try p <|> q` will try `q` even when
|
||||
`p` has consumed input.
|
||||
|
||||
It is also useful for specifying both the lexer and Parser
|
||||
together.
|
||||
```
|
||||
(do try (ch 'l' >> ch 'e' >> ch 't'), whitespace, ...)
|
||||
<|>
|
||||
...
|
||||
```
|
||||
Without the `try` Combinator we will not be able to backtrack on the `let` keyword.
|
||||
-/
|
||||
@[inline] def try (p : ParsecT μ m α) : ParsecT μ m α :=
|
||||
λ it, do
|
||||
r ← p it,
|
||||
pure $ tryMkRes r
|
||||
|
||||
@[inlineIfReduce] def orelseMkRes (msg₁ : Message μ) (r : Result μ α) : Result μ α :=
|
||||
match r with
|
||||
| ok a it' (some ex₂) := ok a it' (some $ msg₁.expected ++ ex₂)
|
||||
| error msg₂ false := error (merge msg₁ msg₂) false
|
||||
| other := other
|
||||
|
||||
/--
|
||||
The `orelse p q` Combinator behaves as follows:
|
||||
1- If `p` succeeds *or* consumes input, return
|
||||
its Result. Otherwise, execute `q` and return its
|
||||
Result.
|
||||
Recall that the `try p` Combinator can be used to
|
||||
pretend that `p` did not consume any input, and
|
||||
simulate infinite lookahead.
|
||||
2- If both `p` and `q` did not consume any input, then
|
||||
combine their error messages (even if one of
|
||||
them succeeded).
|
||||
-/
|
||||
@[inline] protected def orelse (p q : ParsecT μ m α) : ParsecT μ m α :=
|
||||
λ it, do
|
||||
r ← p it,
|
||||
match r with
|
||||
| error msg₁ false := do { r ← q it, pure $ orelseMkRes msg₁ r }
|
||||
| other := pure other
|
||||
|
||||
instance : Alternative (ParsecT μ m) :=
|
||||
{ orelse := λ _, ParsecT.orelse,
|
||||
failure := λ _, ParsecT.failure,
|
||||
..ParsecT.Monad }
|
||||
|
||||
/-- Run `p`, but do not consume any input when `p` succeeds. -/
|
||||
@[specialize] def lookahead (p : ParsecT μ m α) : ParsecT μ m α :=
|
||||
λ it, do
|
||||
r ← p it,
|
||||
pure $ match r with
|
||||
| ok a s' _ := mkEps a it
|
||||
| other := other
|
||||
end ParsecT
|
||||
|
||||
/- Type class for abstracting from concrete Monad stacks containing a `Parsec` somewhere. -/
|
||||
class MonadParsec (μ : outParam Type) (m : Type → Type) :=
|
||||
-- analogous to e.g. `MonadReader.lift` before simplification (see there)
|
||||
(lift {} {α : Type} : Parsec μ α → m α)
|
||||
-- Analogous to e.g. `MonadReaderAdapter.map` before simplification (see there).
|
||||
-- Its usage seems to be way too common to justify moving it into a separate type class.
|
||||
(map {} {α : Type} : (∀ {m'} [Monad m'] {α}, ParsecT μ m' α → ParsecT μ m' α) → m α → m α)
|
||||
|
||||
/-- `Parsec` without custom error Message Type -/
|
||||
abbrev MonadParsec' := MonadParsec Unit
|
||||
|
||||
variables {μ : Type}
|
||||
|
||||
instance {m : Type → Type} [Monad m] : MonadParsec μ (ParsecT μ m) :=
|
||||
{ lift := λ α p it, pure (p it),
|
||||
map := λ α f x, f x }
|
||||
|
||||
instance monadParsecTrans {m n : Type → Type} [HasMonadLift m n] [MonadFunctor m m n n] [MonadParsec μ m] : MonadParsec μ n :=
|
||||
{ lift := λ α p, monadLift (MonadParsec.lift p : m α),
|
||||
map := λ α f x, monadMap (λ β x, (MonadParsec.map @f x : m β)) x }
|
||||
|
||||
namespace MonadParsec
|
||||
open ParsecT
|
||||
variables {m : Type → Type} [Monad m] [MonadParsec μ m] {α β : Type}
|
||||
|
||||
def error {α : Type} (unexpected : String) (expected : DList String := ∅)
|
||||
(it : Option OldIterator := none) (custom : Option μ := none) : m α :=
|
||||
lift $ λ it', Result.error { unexpected := unexpected, expected := expected, it := it.getOrElse it', custom := custom } false
|
||||
|
||||
@[inline] def leftOver : m OldIterator :=
|
||||
lift $ λ it, Result.mkEps it it
|
||||
|
||||
/-- Return the number of characters left to be parsed. -/
|
||||
@[inline] def remaining : m Nat :=
|
||||
String.OldIterator.remaining <$> leftOver
|
||||
|
||||
@[inline] def labels (p : m α) (lbls : DList String) : m α :=
|
||||
map (λ m' inst β p, @ParsecT.labels m' inst μ β p lbls) p
|
||||
|
||||
@[inline] def label (p : m α) (lbl : String) : m α :=
|
||||
labels p (DList.singleton lbl)
|
||||
|
||||
infixr ` <?> `:2 := label
|
||||
|
||||
@[inline] def hidden (p : m α) : m α :=
|
||||
labels p ∅
|
||||
|
||||
/--
|
||||
`try p` behaves like `p`, but it pretends `p` hasn't
|
||||
consumed any input when `p` fails.
|
||||
|
||||
It is useful for implementing infinite lookahead.
|
||||
The Parser `try p <|> q` will try `q` even when
|
||||
`p` has consumed input.
|
||||
|
||||
It is also useful for specifying both the lexer and Parser
|
||||
together.
|
||||
```
|
||||
(do try (ch 'l' >> ch 'e' >> ch 't'), whitespace, ...)
|
||||
<|>
|
||||
...
|
||||
```
|
||||
Without the `try` Combinator we will not be able to backtrack on the `let` keyword.
|
||||
-/
|
||||
|
||||
@[inline] def try (p : m α) : m α :=
|
||||
map (λ m' inst β p, @ParsecT.try m' inst μ β p) p
|
||||
|
||||
/-- Parse `p` without consuming any input. -/
|
||||
@[inline] def lookahead (p : m α) : m α :=
|
||||
map (λ m' inst β p, @ParsecT.lookahead m' inst μ β p) p
|
||||
|
||||
/-- Faster version of `notFollowedBy (satisfy p)` -/
|
||||
@[inline] def notFollowedBySat (p : Char → Bool) : m Unit :=
|
||||
do it ← leftOver,
|
||||
if !it.hasNext then pure ()
|
||||
else let c := it.curr in
|
||||
if p c then error (repr c)
|
||||
else pure ()
|
||||
|
||||
def eoiError (it : OldIterator) : Result μ α :=
|
||||
Result.error { it := it, unexpected := "end of input", custom := default _ } false
|
||||
|
||||
def curr : m Char :=
|
||||
String.OldIterator.curr <$> leftOver
|
||||
|
||||
@[inline] def cond (p : Char → Bool) (t : m α) (e : m α) : m α :=
|
||||
mcond (p <$> curr) t e
|
||||
|
||||
/--
|
||||
If the next character `c` satisfies `p`, then
|
||||
update Position and return `c`. Otherwise,
|
||||
generate error Message with current Position and character. -/
|
||||
@[inline] def satisfy (p : Char → Bool) : m Char :=
|
||||
do it ← leftOver,
|
||||
if !it.hasNext then error "end of input"
|
||||
else let c := it.curr in
|
||||
if p c then lift $ λ _, Result.ok c it.next none
|
||||
else error (repr c)
|
||||
|
||||
def ch (c : Char) : m Char :=
|
||||
satisfy (= c)
|
||||
|
||||
def alpha : m Char :=
|
||||
satisfy Char.isAlpha
|
||||
|
||||
def digit : m Char :=
|
||||
satisfy Char.isDigit
|
||||
|
||||
def upper : m Char :=
|
||||
satisfy Char.isUpper
|
||||
|
||||
def lower : m Char :=
|
||||
satisfy Char.isLower
|
||||
|
||||
def any : m Char :=
|
||||
satisfy (λ _, True)
|
||||
|
||||
private def strAux : Nat → OldIterator → OldIterator → Option OldIterator
|
||||
| 0 _ it := some it
|
||||
| (n+1) sIt it :=
|
||||
if it.hasNext ∧ sIt.curr = it.curr then strAux n sIt.next it.next
|
||||
else none
|
||||
|
||||
/--
|
||||
`str s` parses a sequence of elements that match `s`. Returns the parsed String (i.e. `s`).
|
||||
This Parser consumes no input if it fails (even if a partial match).
|
||||
Note: The behaviour of this Parser is different to that the `String` Parser in the ParsecT Μ M Haskell library,
|
||||
as this one is all-or-nothing.
|
||||
-/
|
||||
def strCore (s : String) (ex : DList String) : m String :=
|
||||
if s.isEmpty then pure ""
|
||||
else lift $ λ it, match strAux s.length s.mkOldIterator it with
|
||||
| some it' := Result.ok s it' none
|
||||
| none := Result.error { it := it, expected := ex, custom := none } false
|
||||
|
||||
@[inline] def str (s : String) : m String :=
|
||||
strCore s (DList.singleton (repr s))
|
||||
|
||||
private def takeAux : Nat → String → OldIterator → Result μ String
|
||||
| 0 r it := Result.ok r it none
|
||||
| (n+1) r it :=
|
||||
if !it.hasNext then eoiError it
|
||||
else takeAux n (r.push (it.curr)) it.next
|
||||
|
||||
/-- Consume `n` characters. -/
|
||||
def take (n : Nat) : m String :=
|
||||
if n = 0 then pure ""
|
||||
else lift $ takeAux n ""
|
||||
|
||||
private def mkStringResult (r : String) (it : OldIterator) : Result μ String :=
|
||||
if r.isEmpty then Result.mkEps r it
|
||||
else Result.ok r it none
|
||||
|
||||
@[specialize]
|
||||
private def takeWhileAux (p : Char → Bool) : Nat → String → OldIterator → Result μ String
|
||||
| 0 r it := mkStringResult r it
|
||||
| (n+1) r it :=
|
||||
if !it.hasNext then mkStringResult r it
|
||||
else let c := it.curr in
|
||||
if p c then takeWhileAux n (r.push c) it.next
|
||||
else mkStringResult r it
|
||||
|
||||
/--
|
||||
Consume input as long as the predicate returns `true`, and return the consumed input.
|
||||
This Parser does not fail. It will return an Empty String if the predicate
|
||||
returns `false` on the current character. -/
|
||||
@[specialize] def takeWhile (p : Char → Bool) : m String :=
|
||||
lift $ λ it, takeWhileAux p it.remaining "" it
|
||||
|
||||
@[specialize] def takeWhileCont (p : Char → Bool) (ini : String) : m String :=
|
||||
lift $ λ it, takeWhileAux p it.remaining ini it
|
||||
|
||||
/--
|
||||
Consume input as long as the predicate returns `true`, and return the consumed input.
|
||||
This Parser requires the predicate to succeed on at least once. -/
|
||||
@[specialize] def takeWhile1 (p : Char → Bool) : m String :=
|
||||
do c ← satisfy p,
|
||||
takeWhileCont p (toString c)
|
||||
|
||||
/--
|
||||
Consume input as long as the predicate returns `false` (i.e. until it returns `true`), and return the consumed input.
|
||||
This Parser does not fail. -/
|
||||
@[inline] def takeUntil (p : Char → Bool) : m String :=
|
||||
takeWhile (λ c, !p c)
|
||||
|
||||
@[inline] def takeUntil1 (p : Char → Bool) : m String :=
|
||||
takeWhile1 (λ c, !p c)
|
||||
|
||||
private def mkConsumedResult (consumed : Bool) (it : OldIterator) : Result μ Unit :=
|
||||
if consumed then Result.ok () it none
|
||||
else Result.mkEps () it
|
||||
|
||||
@[specialize] private def takeWhileAux' (p : Char → Bool) : Nat → Bool → OldIterator → Result μ Unit
|
||||
| 0 consumed it := mkConsumedResult consumed it
|
||||
| (n+1) consumed it :=
|
||||
if !it.hasNext then mkConsumedResult consumed it
|
||||
else let c := it.curr in
|
||||
if p c then takeWhileAux' n true it.next
|
||||
else mkConsumedResult consumed it
|
||||
|
||||
/-- Similar to `takeWhile` but it does not return the consumed input. -/
|
||||
@[specialize] def takeWhile' (p : Char → Bool) : m Unit :=
|
||||
lift $ λ it, takeWhileAux' p it.remaining false it
|
||||
|
||||
/-- Similar to `takeWhile1` but it does not return the consumed input. -/
|
||||
@[specialize] def takeWhile1' (p : Char → Bool) : m Unit :=
|
||||
satisfy p *> takeWhile' p
|
||||
|
||||
/-- Consume zero or more whitespaces. -/
|
||||
@[noinline] def whitespace : m Unit :=
|
||||
takeWhile' Char.isWhitespace
|
||||
|
||||
/-- Shorthand for `p <* whitespace` -/
|
||||
@[inline] def lexeme (p : m α) : m α :=
|
||||
p <* whitespace
|
||||
|
||||
/-- Parse a numeral in decimal. -/
|
||||
@[noinline] def num : m Nat :=
|
||||
String.toNat <$> (takeWhile1 Char.isDigit)
|
||||
|
||||
/-- Succeed only if there are at least `n` characters left. -/
|
||||
def ensure (n : Nat) : m Unit :=
|
||||
do it ← leftOver,
|
||||
if n ≤ it.remaining then pure ()
|
||||
else error "end of input" (DList.singleton ("at least " ++ toString n ++ " characters"))
|
||||
|
||||
/-- Return the current Position. -/
|
||||
def pos : m Position :=
|
||||
String.OldIterator.offset <$> leftOver
|
||||
|
||||
|
||||
/-- `notFollowedBy p` succeeds when Parser `p` fails -/
|
||||
@[inline] def notFollowedBy [MonadExcept (Message μ) m] (p : m α) (msg : String := "input") : m Unit :=
|
||||
do it ← leftOver,
|
||||
b ← lookahead $ catch (p *> pure false) (λ _, pure true),
|
||||
if b then pure () else error msg ∅ it
|
||||
|
||||
def eoi : m Unit :=
|
||||
do it ← leftOver,
|
||||
if it.remaining = 0 then pure ()
|
||||
else error (repr it.curr) (DList.singleton ("end of input"))
|
||||
|
||||
@[specialize] def many1Aux [Alternative m] (p : m α) : Nat → m (List α)
|
||||
| 0 := do a ← p, pure [a]
|
||||
| (n+1) := do a ← p,
|
||||
as ← (many1Aux n <|> pure []),
|
||||
pure (a::as)
|
||||
|
||||
@[specialize] def many1 [Alternative m] (p : m α) : m (List α) :=
|
||||
do r ← remaining, many1Aux p r
|
||||
|
||||
@[specialize] def many [Alternative m] (p : m α) : m (List α) :=
|
||||
many1 p <|> pure []
|
||||
|
||||
@[specialize] def many1Aux' [Alternative m] (p : m α) : Nat → m Unit
|
||||
| 0 := p *> pure ()
|
||||
| (n+1) := p *> (many1Aux' n <|> pure ())
|
||||
|
||||
@[inline] def many1' [Alternative m] (p : m α) : m Unit :=
|
||||
do r ← remaining, many1Aux' p r
|
||||
|
||||
@[specialize] def many' [Alternative m] (p : m α) : m Unit :=
|
||||
many1' p <|> pure ()
|
||||
|
||||
@[specialize] def sepBy1 [Alternative m] (p : m α) (sep : m β) : m (List α) :=
|
||||
(::) <$> p <*> many (sep *> p)
|
||||
|
||||
@[specialize] def SepBy [Alternative m] (p : m α) (sep : m β) : m (List α) :=
|
||||
sepBy1 p sep <|> pure []
|
||||
|
||||
@[specialize] def fixAux [Alternative m] (f : m α → m α) : Nat → m α
|
||||
| 0 := error "fixAux: no progress"
|
||||
| (n+1) := f (fixAux n)
|
||||
|
||||
@[specialize] def fix [Alternative m] (f : m α → m α) : m α :=
|
||||
do n ← remaining, fixAux f (n+1)
|
||||
|
||||
@[specialize] def foldrAux [Alternative m] (f : α → β → β) (p : m α) (b : β) : Nat → m β
|
||||
| 0 := pure b
|
||||
| (n+1) := (f <$> p <*> foldrAux n) <|> pure b
|
||||
|
||||
/-- Matches zero or more occurrences of `p`, and folds the Result. -/
|
||||
@[specialize] def foldr [Alternative m] (f : α → β → β) (p : m α) (b : β) : m β :=
|
||||
do it ← leftOver,
|
||||
foldrAux f p b it.remaining
|
||||
|
||||
@[specialize] def foldlAux [Alternative m] (f : α → β → α) (p : m β) : α → Nat → m α
|
||||
| a 0 := pure a
|
||||
| a (n+1) := (do x ← p, foldlAux (f a x) n) <|> pure a
|
||||
|
||||
/-- Matches zero or more occurrences of `p`, and folds the Result. -/
|
||||
@[specialize] def foldl [Alternative m] (f : α → β → α) (a : α) (p : m β) : m α :=
|
||||
do it ← leftOver,
|
||||
foldlAux f p a it.remaining
|
||||
|
||||
def unexpected (msg : String) : m α :=
|
||||
error msg
|
||||
|
||||
def unexpectedAt (msg : String) (it : OldIterator) : m α :=
|
||||
error msg ∅ it
|
||||
|
||||
/- Execute all parsers in `ps` and return the Result of the longest parse(s) if any,
|
||||
or else the Result of the furthest error. If there are two parses of
|
||||
equal length, the first parse wins. -/
|
||||
@[specialize]
|
||||
def longestMatch [MonadExcept (Message μ) m] (ps : List (m α)) : m (List α) :=
|
||||
do it ← leftOver,
|
||||
r ← ps.mfoldr (λ p (r : Result μ (List α)),
|
||||
lookahead $ catch
|
||||
(do
|
||||
a ← p,
|
||||
it ← leftOver,
|
||||
pure $ match r with
|
||||
| Result.ok as it' none := if it'.offset > it.offset then r
|
||||
else if it.offset > it'.offset then Result.ok [a] it none
|
||||
else Result.ok (a::as) it none
|
||||
| _ := Result.ok [a] it none)
|
||||
(λ msg, pure $ match r with
|
||||
| Result.error msg' _ := if msg'.it.offset > msg.it.offset then r
|
||||
else if msg.it.offset > msg'.it.offset then Result.error msg true
|
||||
else Result.error (merge msg msg') (msg.it.offset > it.offset)
|
||||
| _ := r))
|
||||
((error "longestMatch: Empty List" : Parsec _ _) it),
|
||||
lift $ λ _, r
|
||||
|
||||
@[specialize]
|
||||
def observing [MonadExcept (Message μ) m] (p : m α) : m (Except (Message μ) α) :=
|
||||
catch (Except.ok <$> p) $ λ msg, pure (Except.error msg)
|
||||
|
||||
end MonadParsec
|
||||
|
||||
namespace MonadParsec
|
||||
open ParsecT
|
||||
variables {m : Type → Type} [Monad m] [MonadParsec Unit m] {α β : Type}
|
||||
|
||||
end MonadParsec
|
||||
|
||||
namespace ParsecT
|
||||
open MonadParsec
|
||||
variables {m : Type → Type} [Monad m] {α β : Type}
|
||||
|
||||
def parse (p : ParsecT μ m α) (s : String) (fname := "") : m (Except (Message μ) α) :=
|
||||
run p s fname
|
||||
|
||||
def parseWithEoi (p : ParsecT μ m α) (s : String) (fname := "") : m (Except (Message μ) α) :=
|
||||
run (p <* eoi) s fname
|
||||
|
||||
def parseWithLeftOver (p : ParsecT μ m α) (s : String) (fname := "") : m (Except (Message μ) (α × OldIterator)) :=
|
||||
run (Prod.mk <$> p <*> leftOver) s fname
|
||||
|
||||
end ParsecT
|
||||
|
||||
def Parsec.parse {α : Type} (p : Parsec μ α) (s : String) (fname := "") : Except (Message μ) α :=
|
||||
ParsecT.parse p s fname
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,56 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
A Combinator for building Pratt parsers
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.token
|
||||
|
||||
namespace Lean.Parser
|
||||
open MonadParsec Combinators
|
||||
|
||||
variables {baseM : Type → Type}
|
||||
variables [Monad baseM] [monadBasicParser baseM] [MonadParsec Syntax baseM] [MonadReader ParserConfig baseM]
|
||||
|
||||
local notation `m` := RecT Nat Syntax baseM
|
||||
local notation `Parser` := m Syntax
|
||||
|
||||
def currLbp : m Nat :=
|
||||
do Except.ok tk ← monadLift peekToken | pure 0,
|
||||
match tk with
|
||||
| Syntax.atom ⟨_, sym⟩ := do
|
||||
cfg ← read,
|
||||
some ⟨_, tkCfg⟩ ← pure (cfg.tokens.oldMatchPrefix sym.mkOldIterator) | error "currLbp: unreachable",
|
||||
pure tkCfg.lbp
|
||||
| Syntax.ident _ := pure maxPrec
|
||||
| Syntax.rawNode {kind := @number, ..} := pure maxPrec
|
||||
| Syntax.rawNode {kind := @stringLit, ..} := pure maxPrec
|
||||
| _ := error "currLbp: unknown token kind"
|
||||
|
||||
private def trailingLoop (trailing : ReaderT Syntax m Syntax) (rbp : Nat) : Nat → Syntax → Parser
|
||||
| 0 _ := error "unreachable"
|
||||
| (n+1) left := do
|
||||
lbp ← currLbp,
|
||||
if rbp < lbp then do
|
||||
left ← trailing.run left,
|
||||
trailingLoop n left
|
||||
else
|
||||
pure left
|
||||
|
||||
variables [MonadExcept (Parsec.Message Syntax) baseM] [Alternative baseM]
|
||||
variables (leading : m Syntax) (trailing : ReaderT Syntax m Syntax) (p : m Syntax)
|
||||
|
||||
def prattParser : baseM Syntax :=
|
||||
RecT.runParsec p $ λ rbp, do
|
||||
left ← leading,
|
||||
n ← remaining,
|
||||
trailingLoop trailing rbp (n+1) left
|
||||
|
||||
instance prattParser.tokens [HasTokens leading] [HasTokens trailing] : HasTokens (prattParser leading trailing p) :=
|
||||
⟨HasTokens.tokens leading ++ HasTokens.tokens trailing⟩
|
||||
instance prattParser.View : HasView Syntax (prattParser leading trailing p) :=
|
||||
default _
|
||||
|
||||
end Lean.Parser
|
||||
|
|
@ -1,56 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Recursion monad transformer
|
||||
-/
|
||||
prelude
|
||||
import init.control.reader init.lean.parser.parsec init.fix
|
||||
|
||||
namespace Lean.Parser
|
||||
|
||||
/-- A small wrapper of `ReaderT` that simplifies introducing and invoking
|
||||
recursion points in a computation. -/
|
||||
def RecT (α δ : Type) (m : Type → Type) (β : Type) :=
|
||||
ReaderT (α → m δ) m β
|
||||
|
||||
namespace RecT
|
||||
variables {m : Type → Type} {α δ β : Type} [Monad m]
|
||||
local attribute [reducible] RecT
|
||||
|
||||
/-- Continue at the recursion point stored at `run`. -/
|
||||
@[inline] def recurse (a : α) : RecT α δ m δ :=
|
||||
λ f, f a
|
||||
|
||||
/-- Execute `x`, executing `rec a` whenever `recurse a` is called.
|
||||
After `maxRec` recursion steps, `base` is executed instead. -/
|
||||
@[inline] protected def run (x : RecT α δ m β) (base : α → m δ) (rec : α → RecT α δ m δ) : m β :=
|
||||
x (fixCore base (λ a f, rec f a))
|
||||
|
||||
@[inline] protected def runParsec {γ : Type} [MonadParsec γ m] (x : RecT α δ m β) (rec : α → RecT α δ m δ) : m β :=
|
||||
RecT.run x (λ _, MonadParsec.error "RecT.runParsec: no progress") rec
|
||||
|
||||
-- not clear how to auto-derive these given the additional constraints
|
||||
instance : Monad (RecT α δ m) := inferInstance
|
||||
instance [Alternative m] : Alternative (RecT α δ m) := inferInstance
|
||||
instance : HasMonadLift m (RecT α δ m) := inferInstance
|
||||
instance (ε) [MonadExcept ε m] : MonadExcept ε (RecT α δ m) := inferInstance
|
||||
instance (μ) [MonadParsec μ m] : MonadParsec μ (RecT α δ m) :=
|
||||
inferInstance
|
||||
-- NOTE: does not allow to vary `m` because of its occurrence in the Reader State
|
||||
instance [Monad m] : MonadFunctor m m (RecT α δ m) (RecT α δ m) :=
|
||||
inferInstance
|
||||
end RecT
|
||||
|
||||
class MonadRec (α δ : outParam Type) (m : Type → Type) :=
|
||||
(recurse {} : α → m δ)
|
||||
export MonadRec (recurse)
|
||||
|
||||
instance MonadRec.trans (α δ m m') [HasMonadLift m m'] [MonadRec α δ m] [Monad m] : MonadRec α δ m' :=
|
||||
{ recurse := λ a, monadLift (recurse a : m δ) }
|
||||
|
||||
instance MonadRec.base (α δ m) [Monad m] : MonadRec α δ (RecT α δ m) :=
|
||||
{ recurse := RecT.recurse }
|
||||
|
||||
end Lean.Parser
|
||||
|
|
@ -1,54 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Leonardo de Moura
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.parsec
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
open MonadParsec
|
||||
variables {m : Type → Type} {μ : Type} [Monad m] [MonadParsec μ m] [Alternative m]
|
||||
|
||||
def parseHexDigit : m Nat :=
|
||||
( (do d ← digit, pure $ d.toNat - '0'.toNat)
|
||||
<|> (do c ← satisfy (λ c, 'a'.val ≤ c.val && c.val ≤ 'f'.val), pure $ 10 + (c.toNat - 'a'.toNat))
|
||||
<|> (do c ← satisfy (λ c, 'A'.val ≤ c.val && c.val ≤ 'F'.val), pure $ 10 + (c.toNat - 'A'.toNat)))
|
||||
<?> "hexadecimal"
|
||||
|
||||
def parseQuotedChar : m Char :=
|
||||
do it ← leftOver,
|
||||
c ← any,
|
||||
if c = '\\' then pure '\\'
|
||||
else if c = '\"' then pure '\"'
|
||||
else if c = '\'' then pure '\''
|
||||
else if c = 'n' then pure '\n'
|
||||
else if c = 't' then pure '\t'
|
||||
else if c = 'x' then do {
|
||||
d₁ ← parseHexDigit,
|
||||
d₂ ← parseHexDigit,
|
||||
pure $ Char.ofNat (16*d₁ + d₂) }
|
||||
else if c = 'u' then do {
|
||||
d₁ ← parseHexDigit,
|
||||
d₂ ← parseHexDigit,
|
||||
d₃ ← parseHexDigit,
|
||||
d₄ ← parseHexDigit,
|
||||
pure $ Char.ofNat (16*(16*(16*d₁ + d₂) + d₃) + d₄) }
|
||||
else unexpectedAt "quoted character" it
|
||||
|
||||
def parseStringLiteralAux : Nat → String → m String
|
||||
| 0 s := ch '\"' *> pure s
|
||||
| (n+1) s := do
|
||||
c ← any,
|
||||
if c = '\\' then do c ← parseQuotedChar, parseStringLiteralAux n (s.push c)
|
||||
else if c = '\"' then pure s
|
||||
else parseStringLiteralAux n (s.push c)
|
||||
|
||||
def parseStringLiteral : m String :=
|
||||
do ch '\"',
|
||||
r ← remaining,
|
||||
parseStringLiteralAux r ""
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,222 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
-/
|
||||
prelude
|
||||
import init.lean.name init.lean.parser.parsec
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
--TODO(Sebastian): move
|
||||
structure Substring :=
|
||||
(start : String.OldIterator)
|
||||
(stop : String.OldIterator)
|
||||
|
||||
structure SourceInfo :=
|
||||
/- Will be inferred after parsing by `Syntax.updateLeading`. During parsing,
|
||||
it is not at all clear what the preceding token was, especially with backtracking. -/
|
||||
(leading : Substring)
|
||||
(pos : Parsec.Position)
|
||||
(trailing : Substring)
|
||||
|
||||
structure SyntaxAtom :=
|
||||
(info : Option SourceInfo := none) (val : String)
|
||||
|
||||
/-- A simple wrapper that should remind you to use the static declaration instead
|
||||
of hard-coding the Node Name. -/
|
||||
structure SyntaxNodeKind :=
|
||||
-- should be equal to the Name of the declaration this structure instance was bound to
|
||||
(name : Name)
|
||||
|
||||
/-- Signifies ambiguous Syntax to be disambiguated by the Elaborator. Should have at least two children.
|
||||
|
||||
This Node kind is special-cased by `Syntax.reprint` since its children's outputs should not be concatenated. -/
|
||||
@[pattern] def choice : SyntaxNodeKind := ⟨`Lean.Parser.choice⟩
|
||||
/-- A nondescriptive kind that can be used for merely grouping Syntax trees into a Node.
|
||||
|
||||
This Node kind is special-cased by `Syntax.Format` to be printed as brackets `[...]` without a Node kind. -/
|
||||
@[pattern] def noKind : SyntaxNodeKind := ⟨`Lean.Parser.noKind⟩
|
||||
|
||||
/-- A hygiene marker introduced by a macro expansion. -/
|
||||
@[derive DecidableEq HasFormat]
|
||||
def MacroScope := Nat
|
||||
abbrev macroScopes := List MacroScope
|
||||
|
||||
/-
|
||||
Parsers create `SyntaxNode`'s with the following properties (see implementation of `Combinators.Node`):
|
||||
- If `args` contains a `Syntax.missing`, then all subsequent elements are also `Syntax.missing`.
|
||||
- The first argument in `args` is not `Syntax.missing`
|
||||
|
||||
Remark: We do create `SyntaxNode`'s with an Empty `args` field (e.g. for representing `Option.none`).
|
||||
-/
|
||||
structure SyntaxNode (Syntax : Type) :=
|
||||
(kind : SyntaxNodeKind)
|
||||
(args : List Syntax)
|
||||
-- Lazily propagated scopes. Scopes are pushed inwards when a Node is destructed via `Syntax.asNode`,
|
||||
-- until an ident or an atom (in which the scopes vanish) is reached.
|
||||
-- Scopes are stored in a stack with the most recent Scope at the top.
|
||||
(scopes : macroScopes := [])
|
||||
|
||||
structure SyntaxIdent :=
|
||||
(info : Option SourceInfo := none)
|
||||
(rawVal : Substring)
|
||||
(val : Name)
|
||||
/- A List of overloaded, global names that this identifier could have referred to in the lexical context
|
||||
where it was parsed.
|
||||
If the identifier does not resolve to a local binding, it should instead resolve to one of
|
||||
these preresolved constants. -/
|
||||
(preresolved : List Name := [])
|
||||
(scopes : macroScopes := [])
|
||||
|
||||
inductive Syntax
|
||||
| atom (val : SyntaxAtom)
|
||||
| ident (val : SyntaxIdent)
|
||||
-- note: use `Syntax.asNode` instead of matching against this Constructor so that
|
||||
-- macro scopes are propagated
|
||||
| rawNode (val : SyntaxNode Syntax)
|
||||
| missing
|
||||
|
||||
instance : Inhabited Syntax :=
|
||||
⟨Syntax.missing⟩
|
||||
|
||||
def Substring.toString (s : Substring) : String :=
|
||||
s.start.extract s.stop
|
||||
|
||||
def Substring.ofString (s : String) : Substring :=
|
||||
⟨s.mkOldIterator, s.mkOldIterator.toEnd⟩
|
||||
|
||||
instance Substring.HasToString : HasToString Substring :=
|
||||
⟨Substring.toString⟩
|
||||
|
||||
-- TODO(Sebastian): exhaustively argue why (if?) this is correct
|
||||
-- The basic idea is List concatenation with elimination of adjacent identical scopes
|
||||
def macroScopes.flip : macroScopes → macroScopes → macroScopes
|
||||
| ys (x::xs) := match macroScopes.flip ys xs with
|
||||
| y::ys := if x = y then ys else x::y::ys
|
||||
| [] := [x]
|
||||
| ys [] := ys
|
||||
|
||||
namespace Syntax
|
||||
open Lean.Format
|
||||
|
||||
def flipScopes (scopes : macroScopes) : Syntax → Syntax
|
||||
| (Syntax.ident n) := Syntax.ident {n with scopes := n.scopes.flip scopes}
|
||||
| (Syntax.rawNode n) := Syntax.rawNode {n with scopes := n.scopes.flip scopes}
|
||||
| stx := stx
|
||||
|
||||
def mkNode (kind : SyntaxNodeKind) (args : List Syntax) :=
|
||||
Syntax.rawNode { kind := kind, args := args }
|
||||
|
||||
/-- Match against `Syntax.rawNode`, propagating lazy macro scopes. -/
|
||||
def asNode : Syntax → Option (SyntaxNode Syntax)
|
||||
| (Syntax.rawNode n) := some {n with args := n.args.map (flipScopes n.scopes), scopes := []}
|
||||
| _ := none
|
||||
|
||||
protected def list (args : List Syntax) :=
|
||||
mkNode noKind args
|
||||
|
||||
def kind : Syntax → Option SyntaxNodeKind
|
||||
| (Syntax.rawNode n) := some n.kind
|
||||
| _ := none
|
||||
|
||||
def isOfKind (k : SyntaxNodeKind) : Syntax → Bool
|
||||
| (Syntax.rawNode n) := k.name = n.kind.name
|
||||
| _ := false
|
||||
|
||||
section
|
||||
variables {m : Type → Type} [Monad m] (r : Syntax → m (Option Syntax))
|
||||
|
||||
partial def mreplace : Syntax → m Syntax
|
||||
| stx@(rawNode n) := do
|
||||
o ← r stx,
|
||||
match o with
|
||||
| some stx' := pure stx'
|
||||
| none := do args' ← n.args.mmap mreplace, pure $ rawNode {n with args := args'}
|
||||
| stx := do
|
||||
o ← r stx,
|
||||
pure $ o.getOrElse stx
|
||||
|
||||
def replace := @mreplace Id _
|
||||
end
|
||||
|
||||
/- Remark: the State `String.Iterator` is the `SourceInfo.trailing.stop` of the previous token,
|
||||
or the beginning of the String. -/
|
||||
private def updateLeadingAux : Syntax → State String.OldIterator (Option Syntax)
|
||||
| (atom a@{info := some info, ..}) := do
|
||||
last ← get,
|
||||
set info.trailing.stop,
|
||||
pure $ some $ atom {a with info := some {info with leading := ⟨last, last.nextn (info.pos - last.offset)⟩}}
|
||||
| (ident id@{info := some info, ..}) := do
|
||||
last ← get,
|
||||
set info.trailing.stop,
|
||||
pure $ some $ ident {id with info := some {info with leading := ⟨last, last.nextn (info.pos - last.offset)⟩}}
|
||||
| _ := pure none
|
||||
|
||||
/-- Set `SourceInfo.leading` according to the trailing stop of the preceding token.
|
||||
The Result is a round-tripping Syntax tree IF, in the input Syntax tree,
|
||||
* all leading stops, atom contents, and trailing starts are correct
|
||||
* trailing stops are between the trailing start and the next leading stop.
|
||||
|
||||
Remark: after parsing all `SourceInfo.leading` fields are Empty.
|
||||
The Syntax argument is the output produced by the Parser for `source`.
|
||||
This Function "fixes" the `source.leanding` field.
|
||||
|
||||
Note that, the `SourceInfo.trailing` fields are correct.
|
||||
The implementation of this Function relies on this property. -/
|
||||
def updateLeading (source : String) : Syntax → Syntax :=
|
||||
λ stx, Prod.fst $ (mreplace updateLeadingAux stx).run source.mkOldIterator
|
||||
|
||||
/-- Retrieve the left-most leaf's info in the Syntax tree. -/
|
||||
partial def getHeadInfo : Syntax → Option SourceInfo
|
||||
| (atom a) := a.info
|
||||
| (ident id) := id.info
|
||||
| (rawNode n) := n.args.foldr (λ s r, getHeadInfo s <|> r) none
|
||||
| _ := none
|
||||
|
||||
def getPos (stx : Syntax) : Option Parsec.Position :=
|
||||
do i ← stx.getHeadInfo,
|
||||
pure i.pos
|
||||
|
||||
def reprintAtom : SyntaxAtom → String
|
||||
| ⟨some info, s⟩ := info.leading.toString ++ s ++ info.trailing.toString
|
||||
| ⟨none, s⟩ := s
|
||||
|
||||
partial def reprint : Syntax → Option String
|
||||
| (atom ⟨some info, s⟩) := pure $ info.leading.toString ++ s ++ info.trailing.toString
|
||||
| (atom ⟨none, s⟩) := pure s
|
||||
| (ident id@{info := some info, ..}) := pure $ info.leading.toString ++ id.rawVal.toString ++ info.trailing.toString
|
||||
| (ident id@{info := none, ..}) := pure id.rawVal.toString
|
||||
| (rawNode n) :=
|
||||
if n.kind.name = choice.name then match n.args with
|
||||
-- should never happen
|
||||
| [] := failure
|
||||
-- check that every choice prints the same
|
||||
| n::ns := do
|
||||
s ← reprint n,
|
||||
ss ← ns.mmap reprint,
|
||||
guard $ ss.all (= s),
|
||||
pure s
|
||||
else String.join <$> n.args.mmap reprint
|
||||
| missing := ""
|
||||
|
||||
protected partial def format : Syntax → Format
|
||||
| (atom ⟨_, s⟩) := fmt $ repr s
|
||||
| (ident id) :=
|
||||
let scopes := id.preresolved.map fmt ++ id.scopes.reverse.map fmt in
|
||||
let scopes := match scopes with [] := fmt "" | _ := bracket "{" (joinSep scopes ", ") "}" in
|
||||
fmt "`" ++ fmt id.val ++ scopes
|
||||
| stx@(rawNode n) :=
|
||||
let scopes := match n.scopes with [] := fmt "" | _ := bracket "{" (joinSep n.scopes.reverse ", ") "}" in
|
||||
if n.kind.name = `Lean.Parser.noKind then sbracket $ scopes ++ joinSep (n.args.map format) line
|
||||
else let shorterName := n.kind.name.replacePrefix `Lean.Parser Name.anonymous
|
||||
in paren $ joinSep ((fmt shorterName ++ scopes) :: n.args.map format) line
|
||||
| missing := "<missing>"
|
||||
|
||||
instance : HasFormat Syntax := ⟨Syntax.format⟩
|
||||
instance : HasToString Syntax := ⟨toString ∘ fmt⟩
|
||||
end Syntax
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,455 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Term-Level parsers
|
||||
-/
|
||||
prelude
|
||||
import init.lean.parser.level init.lean.parser.notation
|
||||
import init.lean.expr
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
open Combinators Parser.HasView MonadParsec
|
||||
|
||||
local postfix `?`:10000 := optional
|
||||
local postfix *:10000 := Combinators.many
|
||||
local postfix +:10000 := Combinators.many1
|
||||
|
||||
set_option class.instance_max_depth 200
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def identUnivSpec.Parser : basicParser :=
|
||||
node! identUnivSpec [".{", levels: Level.Parser+, "}"]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def identUnivs.Parser : termParser :=
|
||||
node! identUnivs [id: ident.Parser, univs: (monadLift identUnivSpec.Parser)?]
|
||||
|
||||
namespace Term
|
||||
/-- Access leading Term -/
|
||||
def getLeading : trailingTermParser := read
|
||||
instance : HasTokens getLeading := default _
|
||||
instance : HasView Syntax getLeading := default _
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def paren.Parser : termParser :=
|
||||
node! «paren» ["(":maxPrec,
|
||||
content: node! parenContent [
|
||||
Term: Term.Parser,
|
||||
special: nodeChoice! parenSpecial {
|
||||
/- Do not allow trailing comma. Looks a bit weird and would clash with
|
||||
adding support for tuple sections (https://downloads.haskell.org/~ghc/8.2.1/docs/html/usersGuide/glasgowExts.html#tuple-sections). -/
|
||||
tuple: node! tuple [", ", tail: sepBy (Term.Parser 0) (symbol ", ") false],
|
||||
typed: node! typed [" : ", type: Term.Parser],
|
||||
}?,
|
||||
]?,
|
||||
")"
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def hole.Parser : termParser :=
|
||||
node! hole [hole: symbol "_" maxPrec]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def sort.Parser : termParser :=
|
||||
nodeChoice! sort {"Sort":maxPrec, "Type":maxPrec}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def typeSpec.Parser : termParser :=
|
||||
node! typeSpec [" : ", type: Term.Parser 0]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def optType.Parser : termParser :=
|
||||
typeSpec.Parser?
|
||||
|
||||
instance optType.viewDefault : HasViewDefault optType.Parser _ none := ⟨⟩
|
||||
|
||||
section binder
|
||||
@[derive HasTokens HasView]
|
||||
def binderIdent.Parser : termParser :=
|
||||
nodeChoice! binderIdent {id: ident.Parser, hole: hole.Parser}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def binderDefault.Parser : termParser :=
|
||||
nodeChoice! binderDefault {
|
||||
val: node! binderDefaultVal [":=", Term: Term.Parser 0],
|
||||
tac: node! binderDefaultTac [".", Term: Term.Parser 0],
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def binderContent.Parser (requireType := false) : termParser :=
|
||||
node! binderContent [
|
||||
ids: binderIdent.Parser+,
|
||||
type: optional typeSpec.Parser requireType,
|
||||
default: binderDefault.Parser?
|
||||
]
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def simpleBinder.Parser : termParser :=
|
||||
nodeChoice! simpleBinder {
|
||||
explicit: node! simpleExplicitBinder ["(", id: ident.Parser, " : ", type: Term.Parser 0, right: symbol ")"],
|
||||
implicit: node! simpleImplicitBinder ["{", id: ident.Parser, " : ", type: Term.Parser 0, right: symbol "}"],
|
||||
strictImplicit: node! simpleStrictImplicitBinder ["⦃", id: ident.Parser, " : ", type: Term.Parser 0, right: symbol "⦄"],
|
||||
instImplicit: node! simpleInstImplicitBinder ["[", id: ident.Parser, " : ", type: Term.Parser 0, right: symbol "]"],
|
||||
}
|
||||
|
||||
def simpleBinder.View.toBinderInfo : simpleBinder.View → (BinderInfo × SyntaxIdent × Syntax)
|
||||
| (simpleBinder.View.explicit {id := id, type := type}) := (BinderInfo.default, id, type)
|
||||
| (simpleBinder.View.implicit {id := id, type := type}) := (BinderInfo.implicit, id, type)
|
||||
| (simpleBinder.View.strictImplicit {id := id, type := type}) := (BinderInfo.strictImplicit, id, type)
|
||||
| (simpleBinder.View.instImplicit {id := id, type := type}) := (BinderInfo.instImplicit, id, type)
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def anonymousConstructor.Parser : termParser :=
|
||||
node! anonymousConstructor ["⟨":maxPrec, args: sepBy (Term.Parser 0) (symbol ","), "⟩"]
|
||||
|
||||
/- All binders must be surrounded with some kind of bracket. (e.g., '()', '{}', '[]').
|
||||
We use this feature when parsing examples/definitions/theorems. The goal is to avoid counter-intuitive
|
||||
declarations such as:
|
||||
|
||||
example p : False := trivial
|
||||
def main proof : False := trivial
|
||||
|
||||
which would be parsed as
|
||||
|
||||
example (p : False) : _ := trivial
|
||||
|
||||
def main (proof : False) : _ := trivial
|
||||
|
||||
where `_` in both cases is elaborated into `True`. This issue was raised by @gebner in the slack channel.
|
||||
|
||||
|
||||
Remark: we still want implicit delimiters for lambda/pi expressions. That is, we want to
|
||||
write
|
||||
|
||||
fun x : t, s
|
||||
or
|
||||
fun x, s
|
||||
|
||||
instead of
|
||||
|
||||
fun (x : t), s -/
|
||||
@[derive HasTokens HasView]
|
||||
def bracketedBinder.Parser (requireType := false) : termParser :=
|
||||
nodeChoice! bracketedBinder {
|
||||
explicit: node! explicitBinder ["(", content: nodeChoice! explicitBinderContent {
|
||||
«notation»: command.notationLike.Parser,
|
||||
other: binderContent.Parser requireType
|
||||
}, right: symbol ")"],
|
||||
implicit: node! implicitBinder ["{", content: binderContent.Parser, "}"],
|
||||
strictImplicit: node! strictImplicitBinder ["⦃", content: binderContent.Parser, "⦄"],
|
||||
instImplicit: node! instImplicitBinder ["[", content: nodeLongestChoice! instImplicitBinderContent {
|
||||
named: node! instImplicitNamedBinder [id: ident.Parser, " : ", type: Term.Parser 0],
|
||||
anonymous: node! instImplicitAnonymousBinder [type: Term.Parser 0]
|
||||
}, "]"],
|
||||
anonymousConstructor: anonymousConstructor.Parser,
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def binder.Parser : termParser :=
|
||||
nodeChoice! binder {
|
||||
bracketed: bracketedBinder.Parser,
|
||||
unbracketed: binderContent.Parser,
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def bindersExt.Parser : termParser :=
|
||||
node! bindersExt [
|
||||
leadingIds: binderIdent.Parser*,
|
||||
remainder: nodeChoice! bindersRemainder {
|
||||
type: node! bindersTypes [":", type: Term.Parser 0],
|
||||
-- we allow mixing like in `a (b : β) c`, but not `a : α (b : β) c : γ`
|
||||
mixed: nodeChoice! mixedBinder {
|
||||
bracketed: bracketedBinder.Parser,
|
||||
id: binderIdent.Parser,
|
||||
}+,
|
||||
}?
|
||||
]
|
||||
|
||||
/-- We normalize binders to simpler singleton ones during expansion. -/
|
||||
@[derive HasTokens HasView]
|
||||
def binders.Parser : termParser :=
|
||||
nodeChoice! binders {
|
||||
extended: bindersExt.Parser,
|
||||
-- a strict subset of `extended`, so only useful after parsing
|
||||
simple: simpleBinder.Parser,
|
||||
}
|
||||
|
||||
/-- We normalize binders to simpler ones during expansion. These always-bracketed
|
||||
binders are used in declarations and cannot be reduced to nested singleton binders. -/
|
||||
@[derive HasTokens HasView]
|
||||
def bracketedBinders.Parser : termParser :=
|
||||
nodeChoice! bracketedBinders {
|
||||
extended: bracketedBinder.Parser*,
|
||||
-- a strict subset of `extended`, so only useful after parsing
|
||||
simple: simpleBinder.Parser*,
|
||||
}
|
||||
end binder
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def lambda.Parser : termParser :=
|
||||
node! lambda [
|
||||
op: unicodeSymbol "λ" "fun" maxPrec,
|
||||
binders: binders.Parser,
|
||||
",",
|
||||
body: Term.Parser 0
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def assume.Parser : termParser :=
|
||||
node! «assume» [
|
||||
"assume ":maxPrec,
|
||||
binders: nodeChoice! assumeBinders {
|
||||
anonymous: node! assumeAnonymous [": ", type: Term.Parser],
|
||||
binders: binders.Parser
|
||||
},
|
||||
", ",
|
||||
body: Term.Parser 0
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def pi.Parser : termParser :=
|
||||
node! pi [
|
||||
op: anyOf [unicodeSymbol "Π" "Pi" maxPrec, unicodeSymbol "∀" "forall" maxPrec],
|
||||
binders: binders.Parser,
|
||||
",",
|
||||
range: Term.Parser 0
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def explicit.Parser : termParser :=
|
||||
node! explicit [
|
||||
mod: nodeChoice! explicitModifier {
|
||||
explicit: symbol "@" maxPrec,
|
||||
partialExplicit: symbol "@@" maxPrec
|
||||
},
|
||||
id: identUnivs.Parser
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def from.Parser : termParser :=
|
||||
node! «from» ["from ", proof: Term.Parser]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def let.Parser : termParser :=
|
||||
node! «let» [
|
||||
"let ",
|
||||
lhs: nodeChoice! letLhs {
|
||||
id: node! letLhsId [
|
||||
id: ident.Parser,
|
||||
-- NOTE: after expansion, binders are Empty
|
||||
binders: bracketedBinder.Parser*,
|
||||
type: optType.Parser,
|
||||
],
|
||||
pattern: Term.Parser
|
||||
},
|
||||
" := ",
|
||||
value: Term.Parser,
|
||||
" in ",
|
||||
body: Term.Parser,
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def optIdent.Parser : termParser :=
|
||||
(try node! optIdent [id: ident.Parser, " : "])?
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def have.Parser : termParser :=
|
||||
node! «have» [
|
||||
"have ",
|
||||
id: optIdent.Parser,
|
||||
prop: Term.Parser,
|
||||
proof: nodeChoice! haveProof {
|
||||
Term: node! haveTerm [" := ", Term: Term.Parser],
|
||||
«from»: node! haveFrom [", ", «from»: from.Parser],
|
||||
},
|
||||
", ",
|
||||
body: Term.Parser,
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def show.Parser : termParser :=
|
||||
node! «show» [
|
||||
"show ",
|
||||
prop: Term.Parser,
|
||||
", ",
|
||||
«from»: from.Parser,
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def match.Parser : termParser :=
|
||||
node! «match» [
|
||||
"match ",
|
||||
scrutinees: sepBy1 Term.Parser (symbol ", ") false,
|
||||
type: optType.Parser,
|
||||
" with ",
|
||||
optBar: (symbol " | ")?,
|
||||
equations: sepBy1
|
||||
node! «matchEquation» [
|
||||
lhs: sepBy1 Term.Parser (symbol ", ") false, ":=", rhs: Term.Parser]
|
||||
(symbol " | ") false,
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def if.Parser : termParser :=
|
||||
node! «if» [
|
||||
"if ",
|
||||
id: optIdent.Parser,
|
||||
prop: Term.Parser,
|
||||
" then ",
|
||||
thenBranch: Term.Parser,
|
||||
" else ",
|
||||
elseBranch: Term.Parser,
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def structInst.Parser : termParser :=
|
||||
node! structInst [
|
||||
"{":maxPrec,
|
||||
type: (try node! structInstType [id: ident.Parser, " . "])?,
|
||||
«with»: (try node! structInstWith [source: Term.Parser, " with "])?,
|
||||
items: sepBy nodeChoice! structInstItem {
|
||||
field: node! structInstField [id: ident.Parser, " := ", val: Term.Parser],
|
||||
source: node! structInstSource ["..", source: Term.Parser?],
|
||||
} (symbol ", "),
|
||||
"}",
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def Subtype.Parser : termParser :=
|
||||
node! Subtype [
|
||||
"{":maxPrec,
|
||||
id: ident.Parser,
|
||||
type: optType.Parser,
|
||||
"//",
|
||||
prop: Term.Parser,
|
||||
"}"
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def inaccessible.Parser : termParser :=
|
||||
node! inaccessible [".(":maxPrec, Term: Term.Parser, ")"]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def anonymousInaccessible.Parser : termParser :=
|
||||
node! anonymousInaccessible ["._":maxPrec]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def sorry.Parser : termParser :=
|
||||
node! «sorry» ["sorry":maxPrec]
|
||||
|
||||
def borrowPrec := maxPrec - 1
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
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 true, op: unicodeSymbol "→" "->" 25, range: Term.Parser 24]
|
||||
|
||||
-- TODO(Sebastian): replace with attribute
|
||||
@[derive HasTokens]
|
||||
def builtinLeadingParsers : TokenMap termParser := TokenMap.ofList [
|
||||
(`ident, identUnivs.Parser),
|
||||
(number.name, number.Parser),
|
||||
(stringLit.name, stringLit.Parser),
|
||||
("(", paren.Parser),
|
||||
("(", depArrow.Parser),
|
||||
("_", hole.Parser),
|
||||
("Sort", sort.Parser),
|
||||
("Type", sort.Parser),
|
||||
("λ", lambda.Parser),
|
||||
("fun", lambda.Parser),
|
||||
("Π", pi.Parser),
|
||||
("Pi", pi.Parser),
|
||||
("∀", pi.Parser),
|
||||
("forall", pi.Parser),
|
||||
("⟨", anonymousConstructor.Parser),
|
||||
("@", explicit.Parser),
|
||||
("@@", explicit.Parser),
|
||||
("let", let.Parser),
|
||||
("have", have.Parser),
|
||||
("show", show.Parser),
|
||||
("assume", assume.Parser),
|
||||
("match", match.Parser),
|
||||
("if", if.Parser),
|
||||
("{", structInst.Parser),
|
||||
("{", Subtype.Parser),
|
||||
("{", depArrow.Parser),
|
||||
("[", depArrow.Parser),
|
||||
(".(", inaccessible.Parser),
|
||||
("._", anonymousInaccessible.Parser),
|
||||
("sorry", sorry.Parser),
|
||||
("@&", borrowed.Parser)
|
||||
]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def sortApp.Parser : trailingTermParser :=
|
||||
do { l ← getLeading, guard $ l.isOfKind sort } *>
|
||||
node! sortApp [fn: getLeading, Arg: monadLift (Level.Parser maxPrec).run]
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def app.Parser : trailingTermParser :=
|
||||
node! app [fn: getLeading, Arg: Term.Parser maxPrec]
|
||||
|
||||
def mkApp (fn : Syntax) (args : List Syntax) : Syntax :=
|
||||
args.foldl (λ fn Arg, Syntax.mkNode app [fn, Arg]) fn
|
||||
|
||||
@[derive Parser.HasTokens Parser.HasView]
|
||||
def arrow.Parser : trailingTermParser :=
|
||||
node! arrow [dom: getLeading, op: unicodeSymbol "→" "->" 25, range: Term.Parser 24]
|
||||
|
||||
@[derive Parser.HasView]
|
||||
def projection.Parser : trailingTermParser :=
|
||||
try $ node! projection [
|
||||
Term: getLeading,
|
||||
-- do not consume trailing whitespace
|
||||
«.»: rawStr ".",
|
||||
proj: nodeChoice! projectionSpec {
|
||||
id: Parser.ident.Parser,
|
||||
num: number.Parser,
|
||||
},
|
||||
]
|
||||
|
||||
-- register '.' manually because of `rawStr`
|
||||
instance projection.tokens : HasTokens projection.Parser :=
|
||||
/- Use maxPrec + 1 so that it bind more tightly than application:
|
||||
`a (b).c` should be parsed as `a ((b).c)`. -/
|
||||
⟨[{«prefix» := ".", lbp := maxPrec.succ}]⟩
|
||||
|
||||
@[derive HasTokens]
|
||||
def builtinTrailingParsers : TokenMap trailingTermParser := TokenMap.ofList [
|
||||
("→", arrow.Parser),
|
||||
("->", arrow.Parser),
|
||||
(".", projection.Parser)
|
||||
]
|
||||
|
||||
end Term
|
||||
|
||||
private def trailing (cfg : CommandParserConfig) : trailingTermParser :=
|
||||
-- try local parsers first, starting with the newest one
|
||||
(do ps ← indexed cfg.localTrailingTermParsers, ps.foldr (<|>) (error ""))
|
||||
<|>
|
||||
-- next try all non-local parsers
|
||||
(do ps ← indexed cfg.trailingTermParsers, longestMatch ps)
|
||||
<|>
|
||||
-- The application parsers should only be tried as a fall-back;
|
||||
-- e.g. `a + b` should not be parsed as `a (+ b)`.
|
||||
-- TODO(Sebastian): We should be able to remove this workaround using
|
||||
-- the proposed more robust precedence handling
|
||||
anyOf [Term.sortApp.Parser, Term.app.Parser]
|
||||
|
||||
private def leading (cfg : CommandParserConfig) : termParser :=
|
||||
(do ps ← indexed cfg.localLeadingTermParsers, ps.foldr (<|>) (error ""))
|
||||
<|>
|
||||
(do ps ← indexed cfg.leadingTermParsers, longestMatch ps)
|
||||
|
||||
def termParser.run (p : termParser) : commandParser :=
|
||||
do cfg ← read,
|
||||
adaptReader coe $ prattParser (leading cfg) (trailing cfg) p
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
|
|
@ -1,379 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich
|
||||
|
||||
Tokenizer for the Lean language
|
||||
|
||||
Even though our Parser architecture does not statically depend on a tokenizer but works directly on
|
||||
the input String, we still use a "tokenizer" Parser in the Lean Parser in some circumstances:
|
||||
* to distinguish between identifiers and keywords
|
||||
* for error recovery: advance until next command token
|
||||
* ...?
|
||||
-/
|
||||
|
||||
prelude
|
||||
import init.lean.parser.combinators init.lean.parser.stringliteral
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
open MonadParsec Combinators String HasView
|
||||
|
||||
def matchToken : BasicParserM (Option TokenConfig) :=
|
||||
do cfg ← read,
|
||||
it ← leftOver,
|
||||
pure $ Prod.snd <$> cfg.tokens.oldMatchPrefix it
|
||||
|
||||
private def finishCommentBlockAux : Nat → Nat → BasicParserM Unit
|
||||
| nesting (n+1) :=
|
||||
str "/-" *> finishCommentBlockAux (nesting + 1) n
|
||||
<|>
|
||||
str "-/" *> (if nesting = 1 then pure () else finishCommentBlockAux (nesting - 1) n)
|
||||
<|>
|
||||
any *> finishCommentBlockAux nesting n
|
||||
| _ _ := error "unreachable"
|
||||
|
||||
def finishCommentBlock (nesting := 1) : BasicParserM Unit :=
|
||||
do r ← remaining,
|
||||
finishCommentBlockAux nesting (r+1) <?> "end of comment block"
|
||||
|
||||
private def whitespaceAux : Nat → BasicParserM Unit
|
||||
| (n+1) :=
|
||||
do whitespace,
|
||||
str "--" *> takeWhile' (≠ '\n') *> whitespaceAux n
|
||||
<|>
|
||||
-- a "/--" doc comment is an actual token, not whitespace
|
||||
try (str "/-" *> notFollowedBy (str "-")) *> finishCommentBlock *> whitespaceAux n
|
||||
<|>
|
||||
pure ()
|
||||
| 0 := error "unreachable"
|
||||
|
||||
variables {m : Type → Type}
|
||||
local notation `Parser` := m Syntax
|
||||
local notation `lift` := @monadLift BasicParserM _ _ _
|
||||
|
||||
/-- Skip whitespace and comments. -/
|
||||
def whitespace : BasicParserM Unit :=
|
||||
hidden $ do
|
||||
start ← leftOver,
|
||||
-- every `whitespaceAux` loop reads at least one Char
|
||||
whitespaceAux (start.remaining+1)
|
||||
|
||||
section
|
||||
variables [Monad m] [MonadParsec Syntax m]
|
||||
|
||||
@[inline] def asSubstring {α : Type} (p : m α) : m Substring :=
|
||||
do start ← leftOver,
|
||||
p,
|
||||
stop ← leftOver,
|
||||
pure ⟨start, stop⟩
|
||||
|
||||
variables [monadBasicParser m]
|
||||
|
||||
@[specialize] def updateLast (f : Syntax → Syntax) (trailing : Substring) : List Syntax → List Syntax
|
||||
| [] := []
|
||||
| [stx] := [f stx]
|
||||
| (stx::stxs) := stx :: updateLast stxs
|
||||
|
||||
private partial def updateTrailing : Substring → Syntax → Syntax
|
||||
| trailing (Syntax.atom a@⟨some info, _⟩) := Syntax.atom {a with info := some {info with trailing := trailing}}
|
||||
| trailing (Syntax.ident id@{info := some info, ..}) := Syntax.ident {id with info := some {info with trailing := trailing}}
|
||||
| trailing (Syntax.rawNode n) := Syntax.rawNode {n with args := updateLast (updateTrailing trailing) trailing n.args}
|
||||
| trailing stx := stx
|
||||
|
||||
def withTrailing (stx : Syntax) : m Syntax :=
|
||||
do -- TODO(Sebastian): less greedy, more natural whitespace assignment
|
||||
-- E.g. only read up to the next line break
|
||||
trailing ← lift $ asSubstring $ whitespace,
|
||||
pure $ updateTrailing trailing stx
|
||||
|
||||
def mkRawRes (start stop : String.OldIterator) : Syntax :=
|
||||
let ss : Substring := ⟨start, stop⟩ in
|
||||
Syntax.atom ⟨some {leading := ⟨start, start⟩, pos := start.offset, trailing := ⟨stop, stop⟩}, ss.toString⟩
|
||||
|
||||
/-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`. -/
|
||||
@[inline] def raw {α : Type} (p : m α) (trailingWs := false) : Parser := do
|
||||
start ← leftOver,
|
||||
p,
|
||||
stop ← leftOver,
|
||||
let stx := mkRawRes start stop,
|
||||
if trailingWs then withTrailing stx else pure stx
|
||||
|
||||
instance raw.tokens {α} (p : m α) (t) : Parser.HasTokens (raw p t : Parser) := default _
|
||||
instance raw.view {α} (p : m α) (t) : Parser.HasView (Option SyntaxAtom) (raw p t : Parser) :=
|
||||
{ view := λ stx, match stx with
|
||||
| Syntax.atom atom := some atom
|
||||
| _ := none,
|
||||
review := λ a, (Syntax.atom <$> a).getOrElse Syntax.missing }
|
||||
|
||||
/-- Like `raw (str s)`, but default to `s` in views. -/
|
||||
@[inline, derive HasTokens HasView]
|
||||
def rawStr (s : String) (trailingWs := false) : Parser :=
|
||||
raw (str s) trailingWs
|
||||
|
||||
instance rawStr.viewDefault (s) (t) : Parser.HasViewDefault (rawStr s t : Parser) (Option SyntaxAtom) (some {val := s}) :=
|
||||
⟨⟩
|
||||
|
||||
end
|
||||
|
||||
set_option class.instance_max_depth 200
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def detailIdentPart.Parser : BasicParserM Syntax :=
|
||||
nodeChoice! detailIdentPart {
|
||||
escaped: node! detailIdentPartEscaped [
|
||||
escBegin: rawStr idBeginEscape.toString,
|
||||
escaped: raw $ takeUntil1 isIdEndEscape,
|
||||
escEnd: rawStr idEndEscape.toString,
|
||||
],
|
||||
default: raw $ satisfy isIdFirst *> takeWhile isIdRest
|
||||
}
|
||||
|
||||
@[derive HasTokens HasView]
|
||||
def detailIdentSuffix.Parser : RecT Unit Syntax BasicParserM Syntax :=
|
||||
-- consume '.' only when followed by a character starting an detailIdentPart
|
||||
try (lookahead (ch '.' *> (ch idBeginEscape <|> satisfy isIdFirst)))
|
||||
*> node! detailIdentSuffix [«.»: rawStr ".", ident: recurse ()]
|
||||
|
||||
def detailIdent' : RecT Unit Syntax BasicParserM Syntax :=
|
||||
node! detailIdent [part: monadLift detailIdentPart.Parser, suffix: optional detailIdentSuffix.Parser]
|
||||
|
||||
/-- A Parser that gives a more detailed View of `SyntaxIdent.rawVal`. Not used by default for
|
||||
performance reasons. -/
|
||||
def detailIdent.Parser : BasicParserM Syntax :=
|
||||
RecT.runParsec detailIdent' $ λ _, detailIdent'
|
||||
|
||||
private def ident' : basicParser :=
|
||||
do
|
||||
start ← leftOver,
|
||||
s ← idPart,
|
||||
n ← foldl Name.mkString (mkSimpleName s) $ do {
|
||||
-- consume '.' only when followed by a character starting an detailIdentPart
|
||||
try (lookahead (ch '.' *> (ch idBeginEscape <|> satisfy isIdFirst))),
|
||||
ch '.',
|
||||
idPart
|
||||
},
|
||||
stop ← leftOver,
|
||||
pure $ Syntax.ident {
|
||||
info := some {leading := ⟨start, start⟩, pos := start.offset, trailing := ⟨stop, stop⟩},
|
||||
rawVal := ⟨start, stop⟩,
|
||||
val := n
|
||||
}
|
||||
|
||||
-- the Node macro doesn't seem to like these...
|
||||
--TODO(Sebastian): these should probably generate better error messages
|
||||
def parseBinLit : BasicParserM Unit :=
|
||||
ch '0' *> (ch 'b' <|> ch 'B') *> many1' (ch '0' <|> ch '1')
|
||||
|
||||
def parseOctLit : BasicParserM String :=
|
||||
ch '0' *> (ch 'o' <|> ch 'O') *> takeWhile1 (λ c, c ≥ '0' && c < '8')
|
||||
|
||||
def parseHexLit : BasicParserM String :=
|
||||
ch '0' *> (ch 'x' <|> ch 'X') *> takeWhile1 (λ c, c.isDigit || c.isAlpha)
|
||||
|
||||
--TODO(Sebastian): other bases
|
||||
def number' : basicParser :=
|
||||
nodeLongestChoice! number {
|
||||
base10: raw $ takeWhile1 Char.isDigit,
|
||||
base2: raw parseBinLit,
|
||||
base8: raw parseOctLit,
|
||||
base16: raw parseHexLit,
|
||||
}
|
||||
|
||||
def stringLit' : basicParser :=
|
||||
node! stringLit [val: raw parseStringLiteral]
|
||||
|
||||
private def mkConsumeToken (tk : TokenConfig) (it : String.OldIterator) : basicParser :=
|
||||
let it' := it.nextn tk.prefix.length in
|
||||
MonadParsec.lift $ λ _, Parsec.Result.ok (mkRawRes it it') it' none
|
||||
|
||||
def numberOrStringLit : basicParser :=
|
||||
number' <|> stringLit'
|
||||
|
||||
def tokenCont (it : String.OldIterator) (tk : TokenConfig) : basicParser :=
|
||||
do id ← ident',
|
||||
it' ← leftOver,
|
||||
-- if a token is both a symbol and a valid identifier (i.e. a keyword),
|
||||
-- we want it to be recognized as a symbol
|
||||
if it.offset + tk.prefix.length ≥ it'.offset then
|
||||
mkConsumeToken tk it
|
||||
else pure id
|
||||
|
||||
def token : basicParser :=
|
||||
do it ← leftOver,
|
||||
cache ← getCache,
|
||||
-- NOTE: using `catch` instead of `<|>` so that error messages from the second block are preferred
|
||||
catch (do
|
||||
-- check token cache
|
||||
some tkc ← pure cache.tokenCache | failure,
|
||||
guard (it.offset = tkc.startIt.offset),
|
||||
-- hackishly update Parsec Position
|
||||
MonadParsec.lift (λ it, Parsec.Result.ok () tkc.stopIt none),
|
||||
putCache {cache with hit := cache.hit + 1},
|
||||
pure tkc.tk
|
||||
) (λ _, do
|
||||
-- cache failed, update cache
|
||||
|
||||
identStart ← observing $ lookahead (satisfy isIdFirst <|> ch idBeginEscape),
|
||||
tk ← matchToken,
|
||||
tk ← match tk, identStart with
|
||||
| some tk@{suffixParser := some _, ..}, _ :=
|
||||
error "token: not implemented" --str tk *> MonadParsec.lift r
|
||||
| some tk, Except.ok _ := tokenCont it tk
|
||||
| some tk, Except.error _ := mkConsumeToken tk it
|
||||
| none, Except.ok _ := ident'
|
||||
| none, Except.error _ := numberOrStringLit,
|
||||
tk ← withTrailing tk,
|
||||
newIt ← leftOver,
|
||||
putCache {cache with tokenCache := some ⟨it, newIt, tk⟩, miss := cache.miss + 1},
|
||||
pure tk
|
||||
)
|
||||
|
||||
def peekToken : BasicParserM (Except (Parsec.Message Syntax) Syntax) :=
|
||||
observing (try (lookahead token))
|
||||
|
||||
variable [monadBasicParser m]
|
||||
|
||||
def symbolCore (sym : String) (lbp : Nat) (ex : DList String) : Parser :=
|
||||
lift $ try $ do {
|
||||
it ← leftOver,
|
||||
stx@(Syntax.atom ⟨_, sym'⟩) ← token | error "" ex it,
|
||||
when (sym ≠ sym') $
|
||||
error sym' ex it,
|
||||
pure stx
|
||||
} <?> sym
|
||||
|
||||
@[inline] def symbol (sym : String) (lbp := 0) : Parser :=
|
||||
let sym := sym.trim in
|
||||
symbolCore sym lbp (DList.singleton sym)
|
||||
|
||||
instance symbol.tokens (sym lbp) : Parser.HasTokens (symbol sym lbp : Parser) :=
|
||||
⟨[⟨sym.trim, lbp, none⟩]⟩
|
||||
instance symbol.View (sym lbp) : Parser.HasView (Option SyntaxAtom) (symbol sym lbp : Parser) :=
|
||||
{ view := λ stx, match stx with
|
||||
| Syntax.atom atom := some atom
|
||||
| _ := none,
|
||||
review := λ a, (Syntax.atom <$> a).getOrElse Syntax.missing }
|
||||
instance symbol.viewDefault (sym lbp) : Parser.HasViewDefault (symbol sym lbp : Parser) _
|
||||
(some {info := none, val := sym.trim}) := ⟨⟩
|
||||
|
||||
def number.Parser : Parser :=
|
||||
lift $ try $ do {
|
||||
it ← leftOver,
|
||||
stx ← token,
|
||||
if stx.isOfKind number then pure stx
|
||||
else error "" (DList.singleton "number") it
|
||||
}
|
||||
|
||||
instance number.Parser.tokens : Parser.HasTokens (number.Parser : Parser) := default _
|
||||
instance number.Parser.view : Parser.HasView number.View (number.Parser : Parser) :=
|
||||
{..number.HasView}
|
||||
|
||||
private def toNatCore (base : Nat) : String.OldIterator → Nat → Nat → Nat
|
||||
| it 0 r := r
|
||||
| it (i+1) r :=
|
||||
let c := it.curr in
|
||||
let val := if c.isDigit then
|
||||
c.toNat - '0'.toNat
|
||||
else if c ≥ 'a' ∧ c ≤ 'f' then
|
||||
c.toNat - 'a'.toNat
|
||||
else
|
||||
c.toNat - 'A'.toNat in
|
||||
let r := r*base + val in
|
||||
toNatCore it.next i r
|
||||
|
||||
private def toNatBase (s : String) (base : Nat) : Nat :=
|
||||
toNatCore base s.mkOldIterator s.length 0
|
||||
|
||||
def number.View.toNat : number.View → Nat
|
||||
| (number.View.base10 (some atom)) := atom.val.toNat
|
||||
| (number.View.base2 (some atom)) := toNatBase atom.val 2
|
||||
| (number.View.base8 (some atom)) := toNatBase atom.val 8
|
||||
| (number.View.base16 (some atom)) := toNatBase atom.val 16
|
||||
| _ := 1138 -- should never happen, but let's still choose a grep-able number
|
||||
|
||||
def number.View.ofNat (n : Nat) : number.View :=
|
||||
number.View.base10 (some {val := toString n})
|
||||
|
||||
def stringLit.Parser : Parser :=
|
||||
lift $ try $ do {
|
||||
it ← leftOver,
|
||||
stx ← token,
|
||||
some _ ← pure $ tryView stringLit stx | error "" (DList.singleton "String") it,
|
||||
pure stx
|
||||
} <?> "String"
|
||||
|
||||
instance stringLit.Parser.tokens : Parser.HasTokens (stringLit.Parser : Parser) := default _
|
||||
instance stringLit.Parser.View : Parser.HasView stringLit.View (stringLit.Parser : Parser) :=
|
||||
{..stringLit.HasView}
|
||||
|
||||
def stringLit.View.value (lit : stringLit.View) : Option String := do
|
||||
atom ← lit.val,
|
||||
Except.ok s ← pure $ Parsec.parse (parseStringLiteral : Parsec' _) atom.val
|
||||
| failure,
|
||||
pure s
|
||||
|
||||
def ident.Parser : Parser :=
|
||||
lift $ try $ do {
|
||||
it ← leftOver,
|
||||
stx@(Syntax.ident _) ← token | error "" (DList.singleton "identifier") it,
|
||||
pure stx
|
||||
} <?> "identifier"
|
||||
|
||||
instance ident.Parser.tokens : Parser.HasTokens (ident.Parser : Parser) := default _
|
||||
instance ident.Parser.View : Parser.HasView SyntaxIdent (ident.Parser : Parser) :=
|
||||
{ view := λ stx, match stx with
|
||||
| Syntax.ident id := id
|
||||
| _ := {rawVal := Substring.ofString "NOTAnIdent", val := `NOTAnIdent},
|
||||
review := Syntax.ident }
|
||||
|
||||
/-- Read identifier without consulting the token table. -/
|
||||
def rawIdent.Parser : Parser :=
|
||||
lift $ ident' >>= withTrailing
|
||||
|
||||
instance rawIdent.Parser.tokens : Parser.HasTokens (rawIdent.Parser : Parser) := default _
|
||||
instance rawIdent.Parser.View : Parser.HasView SyntaxIdent (rawIdent.Parser : Parser) :=
|
||||
{..(ident.Parser.View : HasView _ (_ : Parser))}
|
||||
|
||||
/-- Check if the following token is the symbol _or_ identifier `sym`. Useful for
|
||||
parsing local tokens that have not been added to the token table (but may have
|
||||
been so by some unrelated code).
|
||||
|
||||
For example, the universe `max` Function is parsed using this Combinator so that
|
||||
it can still be used as an identifier outside of universes (but registering it
|
||||
as a token in a Term Syntax would not break the universe Parser). -/
|
||||
def symbolOrIdent (sym : String) : Parser :=
|
||||
lift $ try $ do
|
||||
it ← leftOver,
|
||||
stx ← token,
|
||||
let sym' := match stx with
|
||||
| Syntax.atom ⟨_, sym'⟩ := some sym'
|
||||
| Syntax.ident id := some id.rawVal.toString
|
||||
| _ := none,
|
||||
when (sym' ≠ some sym) $
|
||||
error "" (DList.singleton (repr sym)) it,
|
||||
pure stx
|
||||
|
||||
instance symbolOrIdent.tokens (sym) : Parser.HasTokens (symbolOrIdent sym : Parser) :=
|
||||
default _
|
||||
instance symbolOrIdent.View (sym) : Parser.HasView Syntax (symbolOrIdent sym : Parser) := default _
|
||||
|
||||
/-- A unicode symbol with an ASCII fallback -/
|
||||
@[derive HasTokens HasView]
|
||||
def unicodeSymbol (unicode ascii : String) (lbp := 0) : Parser :=
|
||||
lift $ anyOf [symbol unicode lbp, symbol ascii lbp]
|
||||
-- use unicode variant by default
|
||||
instance unicodeSymbol.viewDefault (u a lbp) : Parser.HasViewDefault (unicodeSymbol u a lbp : Parser) _ (Syntax.atom ⟨none, u⟩) := ⟨⟩
|
||||
|
||||
def indexed {α : Type} (map : TokenMap α) : m (List α) :=
|
||||
lift $ do
|
||||
Except.ok tk ← peekToken | error "",
|
||||
n ← match tk with
|
||||
| Syntax.atom ⟨_, s⟩ := pure $ mkSimpleName s
|
||||
| Syntax.ident _ := pure `ident
|
||||
| Syntax.rawNode n := pure n.kind.name
|
||||
| _ := error "",
|
||||
Option.toMonad $ map.find n
|
||||
|
||||
end «Parser»
|
||||
end Lean
|
||||
|
|
@ -1,109 +0,0 @@
|
|||
/-
|
||||
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Author: Sebastian Ullrich, Leonardo de Moura
|
||||
|
||||
Trie for tokenizing the Lean language
|
||||
-/
|
||||
prelude
|
||||
import init.data.rbmap
|
||||
import init.lean.format init.lean.parser.parsec
|
||||
|
||||
namespace Lean
|
||||
namespace Parser
|
||||
|
||||
inductive Trie (α : Type)
|
||||
| Node : Option α → RBNode Char (λ _, Trie) → Trie
|
||||
|
||||
namespace Trie
|
||||
variables {α : Type}
|
||||
|
||||
def empty : Trie α :=
|
||||
⟨none, RBNode.leaf⟩
|
||||
|
||||
instance : HasEmptyc (Trie α) :=
|
||||
⟨empty⟩
|
||||
|
||||
instance : Inhabited (Trie α) :=
|
||||
⟨Node none RBNode.leaf⟩
|
||||
|
||||
private partial def insertEmptyAux (s : String) (val : α) : String.Pos → Trie α
|
||||
| i := match s.atEnd i with
|
||||
| true := Trie.Node (some val) RBNode.leaf
|
||||
| false :=
|
||||
let c := s.get i in
|
||||
let t := insertEmptyAux (s.next i) in
|
||||
Trie.Node none (RBNode.singleton c t)
|
||||
|
||||
private partial def insertAux (s : String) (val : α) : Trie α → String.Pos → Trie α
|
||||
| (Trie.Node v m) i :=
|
||||
match s.atEnd i with
|
||||
| true := Trie.Node (some val) m -- overrides old value
|
||||
| false :=
|
||||
let c := s.get i in
|
||||
let i := s.next i in
|
||||
let t := match RBNode.find Char.lt m c with
|
||||
| none := insertEmptyAux s val i
|
||||
| some t := insertAux t i in
|
||||
Trie.Node v (RBNode.insert Char.lt m c t)
|
||||
|
||||
def insert (t : Trie α) (s : String) (val : α) : Trie α :=
|
||||
insertAux s val t 0
|
||||
|
||||
private partial def findAux (s : String) : Trie α → String.Pos → Option α
|
||||
| (Trie.Node val m) i :=
|
||||
match s.atEnd i with
|
||||
| true := val
|
||||
| false :=
|
||||
let c := s.get i in
|
||||
let i := s.next i in
|
||||
match RBNode.find Char.lt m c with
|
||||
| none := none
|
||||
| some t := findAux t i
|
||||
|
||||
def find (t : Trie α) (s : String) : Option α :=
|
||||
findAux s t 0
|
||||
|
||||
private def updtAcc (v : Option α) (i : String.Pos) (acc : String.Pos × Option α) : String.Pos × Option α :=
|
||||
match v, acc with
|
||||
| some v, (j, w) := (i, some v) -- we pattern match on `acc` to enable memory reuse
|
||||
| none, acc := acc
|
||||
|
||||
private partial def matchPrefixAux (s : String) : Trie α → String.Pos → (String.Pos × Option α) → String.Pos × Option α
|
||||
| (Trie.Node v m) i acc :=
|
||||
match s.atEnd i with
|
||||
| true := updtAcc v i acc
|
||||
| false :=
|
||||
let acc := updtAcc v i acc in
|
||||
let c := s.get i in
|
||||
let i := s.next i in
|
||||
match RBNode.find Char.lt m c with
|
||||
| some t := matchPrefixAux t i acc
|
||||
| none := acc
|
||||
|
||||
def matchPrefix (s : String) (t : Trie α) (i : String.Pos) : String.Pos × Option α :=
|
||||
matchPrefixAux s t i (i, none)
|
||||
|
||||
-- TODO: delete
|
||||
private def oldMatchPrefixAux : Nat → Trie α → String.OldIterator → Option (String.OldIterator × α) → Option (String.OldIterator × α)
|
||||
| 0 (Trie.Node val map) it Acc := Prod.mk it <$> val <|> Acc
|
||||
| (n+1) (Trie.Node val map) it Acc :=
|
||||
let Acc' := Prod.mk it <$> val <|> Acc in
|
||||
match RBNode.find Char.lt map it.curr with
|
||||
| some t := oldMatchPrefixAux n t it.next Acc'
|
||||
| none := Acc'
|
||||
|
||||
-- TODO: delete
|
||||
def oldMatchPrefix {α : Type} (t : Trie α) (it : String.OldIterator) : Option (String.OldIterator × α) :=
|
||||
oldMatchPrefixAux it.remaining t it none
|
||||
|
||||
private partial def toStringAux {α : Type} : Trie α → List Format
|
||||
| (Trie.Node val map) := map.fold (λ Fs c t,
|
||||
format (repr c) :: (Format.group $ Format.nest 2 $ flip Format.joinSep Format.line $ toStringAux t) :: Fs) []
|
||||
|
||||
instance {α : Type} : HasToString (Trie α) :=
|
||||
⟨λ t, (flip Format.joinSep Format.line $ toStringAux t).pretty⟩
|
||||
end Trie
|
||||
|
||||
end Parser
|
||||
end Lean
|
||||
Loading…
Add table
Reference in a new issue