From d5612320d726a09fe6a7c305e12de673cd3d180a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 21 Oct 2020 17:12:56 -0700 Subject: [PATCH] chore: move to new frontend --- src/Lean/Server/Snapshots.lean | 105 +++++++++++++++++---------------- 1 file changed, 53 insertions(+), 52 deletions(-) diff --git a/src/Lean/Server/Snapshots.lean b/src/Lean/Server/Snapshots.lean index cf06121ae0..b988e743e3 100644 --- a/src/Lean/Server/Snapshots.lean +++ b/src/Lean/Server/Snapshots.lean @@ -1,3 +1,4 @@ +#lang lean4 /- Copyright (c) 2020 Wojciech Nawrocki. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. @@ -24,34 +25,34 @@ open Elab /-- The data associated with a snapshot is different depending on whether it was produced from the header or from a command. -/ inductive SnapshotData -| headerData : Environment → MessageLog → Options → SnapshotData -| cmdData : Command.State → SnapshotData + | headerData : Environment → MessageLog → Options → SnapshotData + | cmdData : Command.State → SnapshotData /-- What Lean knows about the world after the header and each command. -/ structure Snapshot := -/- Where the command which produced this snapshot begins. Note that -neighbouring snapshots are *not* necessarily attached beginning-to-end, -since inputs outside the grammar advance the parser but do not produce -snapshots. -/ -(beginPos : String.Pos) -(mpState : Parser.ModuleParserState) -(data : SnapshotData) + /- Where the command which produced this snapshot begins. Note that + neighbouring snapshots are *not* necessarily attached beginning-to-end, + since inputs outside the grammar advance the parser but do not produce + snapshots. -/ + (beginPos : String.Pos) + (mpState : Parser.ModuleParserState) + (data : SnapshotData) namespace Snapshot def endPos (s : Snapshot) : String.Pos := s.mpState.pos def env : Snapshot → Environment -| ⟨_, _, SnapshotData.headerData env_ _ _⟩ => env_ -| ⟨_, _, SnapshotData.cmdData cmdState⟩ => cmdState.env + | ⟨_, _, SnapshotData.headerData env_ _ _⟩ => env_ + | ⟨_, _, SnapshotData.cmdData cmdState⟩ => cmdState.env def msgLog : Snapshot → MessageLog -| ⟨_, _, SnapshotData.headerData _ msgLog_ _⟩ => msgLog_ -| ⟨_, _, SnapshotData.cmdData cmdState⟩ => cmdState.messages + | ⟨_, _, SnapshotData.headerData _ msgLog_ _⟩ => msgLog_ + | ⟨_, _, SnapshotData.cmdData cmdState⟩ => cmdState.messages def toCmdState : Snapshot → Command.State -| ⟨_, _, SnapshotData.headerData env msgLog opts⟩ => Command.mkState env msgLog opts -| ⟨_, _, SnapshotData.cmdData cmdState⟩ => cmdState + | ⟨_, _, SnapshotData.headerData env msgLog opts⟩ => Command.mkState env msgLog opts + | ⟨_, _, SnapshotData.cmdData cmdState⟩ => cmdState end Snapshot @@ -59,16 +60,17 @@ end Snapshot -- in some SnapshotsM := ReaderT Context (EIO Empty) def compileHeader (contents : String) (opts : Options := {}) : IO Snapshot := do -let inputCtx := Parser.mkInputContext contents ""; -(headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx; -(headerEnv, msgLog) ← Elab.processHeader headerStx opts msgLog inputCtx; -pure { beginPos := 0, - mpState := headerParserState, - data := SnapshotData.headerData headerEnv msgLog opts - } + let inputCtx := Parser.mkInputContext contents "" + let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx + let (headerEnv, msgLog) ← Elab.processHeader headerStx opts msgLog inputCtx + pure { beginPos := 0, + mpState := headerParserState, + data := SnapshotData.headerData headerEnv msgLog opts + } private def ioErrorFromEmpty (ex : Empty) : IO.Error := -Empty.rec _ ex + nomatch ex + /-- Compiles the next command occurring after the given snapshot. If there is no next command (file ended), returns messages produced @@ -77,40 +79,39 @@ through the file. -/ -- over "store snapshots"/"don't store snapshots" would likely result in confusing -- isServer? conditionals and not be worth it due to how short it is. def compileNextCmd (contents : String) (snap : Snapshot) : IO (Sum Snapshot MessageLog) := do -let inputCtx := Parser.mkInputContext contents ""; -let (cmdStx, cmdParserState, msgLog) := - Parser.parseCommand snap.env inputCtx snap.mpState snap.msgLog; -let cmdPos := cmdStx.getHeadInfo.get!.pos.get!; -- TODO(WN): always `some`? -if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then - pure $ Sum.inr msgLog -else do - cmdStateRef ← IO.mkRef { snap.toCmdState with messages := msgLog }; - let cmdCtx : Elab.Command.Context := - { cmdPos := snap.endPos, - fileName := inputCtx.fileName, - fileMap := inputCtx.fileMap - }; - adaptExcept - ioErrorFromEmpty - (Elab.Command.catchExceptions - (Elab.Command.elabCommand cmdStx) - cmdCtx cmdStateRef); - postCmdState ← cmdStateRef.get; - let postCmdSnap : Snapshot := - { beginPos := cmdPos, - mpState := cmdParserState, - data := SnapshotData.cmdData postCmdState - }; - pure $ Sum.inl postCmdSnap + let inputCtx := Parser.mkInputContext contents ""; + let (cmdStx, cmdParserState, msgLog) := + Parser.parseCommand snap.env inputCtx snap.mpState snap.msgLog; + let cmdPos := cmdStx.getHeadInfo.get!.pos.get!; -- TODO(WN): always `some`? + if Parser.isEOI cmdStx || Parser.isExitCommand cmdStx then + pure $ Sum.inr msgLog + else + let cmdStateRef ← IO.mkRef { snap.toCmdState with messages := msgLog } + let cmdCtx : Elab.Command.Context := { + cmdPos := snap.endPos, + fileName := inputCtx.fileName, + fileMap := inputCtx.fileMap + } + adaptExcept + ioErrorFromEmpty + (Elab.Command.catchExceptions + (Elab.Command.elabCommand cmdStx) + cmdCtx cmdStateRef) + let postCmdState ← cmdStateRef.get + let postCmdSnap : Snapshot := { + beginPos := cmdPos, + mpState := cmdParserState, + data := SnapshotData.cmdData postCmdState + } + pure $ Sum.inl postCmdSnap /-- Compiles all commands after the given snapshot. Returns them as a list, together with the final message log. -/ -partial def compileCmdsAfter (contents : String) : Snapshot → IO (List Snapshot × MessageLog) -| snap => do - cmdOut ← compileNextCmd contents snap; +partial def compileCmdsAfter (contents : String) (snap : Snapshot) : IO (List Snapshot × MessageLog) := do + let cmdOut ← compileNextCmd contents snap match cmdOut with | Sum.inl snap => do - (snaps, msgLog) ← compileCmdsAfter snap; + let (snaps, msgLog) ← compileCmdsAfter contents snap pure $ (snap :: snaps, msgLog) | Sum.inr msgLog => pure ([], msgLog)