From 70c57ce0f09ea9b0c0ff210f560661f4bfdf3dfd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 May 2020 15:50:51 -0700 Subject: [PATCH] chore: update stage0 --- stage0/src/Init/Lean/Attributes.lean | 7 ++++--- stage0/src/Init/Lean/Compiler/IR/Basic.lean | 2 +- stage0/src/Init/Lean/Compiler/IR/Boxing.lean | 2 +- stage0/src/Init/Lean/Data/Options.lean | 2 +- stage0/src/Init/Lean/Elab/Frontend.lean | 2 +- stage0/src/Init/Lean/Elab/Import.lean | 2 +- stage0/src/Init/Lean/Elab/Quotation.lean | 2 +- stage0/src/Init/Lean/Expr.lean | 2 +- stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean | 2 +- stage0/src/Init/Lean/Meta/SynthInstance.lean | 4 ++-- stage0/src/Init/Lean/Parser/Module.lean | 4 ++-- stage0/src/Init/Lean/Parser/Parser.lean | 14 +++++++------- stage0/src/Init/System/FilePath.lean | 2 +- stage0/src/frontends/lean/brackets.cpp | 4 ++++ 14 files changed, 28 insertions(+), 23 deletions(-) diff --git a/stage0/src/Init/Lean/Attributes.lean b/stage0/src/Init/Lean/Attributes.lean index 06b99ea8e3..1716651dc6 100644 --- a/stage0/src/Init/Lean/Attributes.lean +++ b/stage0/src/Init/Lean/Attributes.lean @@ -383,17 +383,18 @@ ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← register r.qsort (fun a b => Name.quickLt a.1 b.1), statsFn := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size }; -let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { AttributeImpl . +let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => { name := name, descr := descr, applicationTime := applicationTime, - add := fun env decl args persistent => do + add := (fun env decl args persistent => do unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent")); unless (env.getModuleIdxFor? decl).isNone $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module")); match validate env decl val with | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg)) - | _ => pure $ ext.addEntry env (decl, val) + | _ => pure $ ext.addEntry env (decl, val)) + : AttributeImpl }; attrs.forM registerBuiltinAttribute; pure { ext := ext, attrs := attrs } diff --git a/stage0/src/Init/Lean/Compiler/IR/Basic.lean b/stage0/src/Init/Lean/Compiler/IR/Basic.lean index df47ec6e9b..a6d7a9e468 100644 --- a/stage0/src/Init/Lean/Compiler/IR/Basic.lean +++ b/stage0/src/Init/Lean/Compiler/IR/Basic.lean @@ -48,7 +48,7 @@ end JoinPointId abbrev MData := KVMap namespace MData -abbrev empty : MData := {KVMap .} +abbrev empty : MData := ({} : KVMap) instance : HasEmptyc MData := ⟨empty⟩ end MData diff --git a/stage0/src/Init/Lean/Compiler/IR/Boxing.lean b/stage0/src/Init/Lean/Compiler/IR/Boxing.lean index 6365424f76..87b1bb0cf5 100644 --- a/stage0/src/Init/Lean/Compiler/IR/Boxing.lean +++ b/stage0/src/Init/Lean/Compiler/IR/Boxing.lean @@ -53,7 +53,7 @@ let ps := decl.params; def mkBoxedVersionAux (decl : Decl) : N Decl := do let ps := decl.params; -qs ← ps.mapM (fun _ => do x ← mkFresh; pure { Param . x := x, ty := IRType.object, borrow := false }); +qs ← ps.mapM (fun _ => do x ← mkFresh; pure { x := x, ty := IRType.object, borrow := false : Param }); (newVDecls, xs) ← qs.size.foldM (fun i (r : Array FnBody × Array Arg) => let (newVDecls, xs) := r; diff --git a/stage0/src/Init/Lean/Data/Options.lean b/stage0/src/Init/Lean/Data/Options.lean index 8667c02222..145bbae172 100644 --- a/stage0/src/Init/Lean/Data/Options.lean +++ b/stage0/src/Init/Lean/Data/Options.lean @@ -14,7 +14,7 @@ namespace Lean def Options := KVMap namespace Options -def empty : Options := {KVMap .} +def empty : Options := ({} : KVMap) instance : HasEmptyc Options := ⟨empty⟩ instance : Inhabited Options := ⟨empty⟩ instance : HasToString Options := inferInstanceAs (HasToString KVMap) diff --git a/stage0/src/Init/Lean/Elab/Frontend.lean b/stage0/src/Init/Lean/Elab/Frontend.lean index 52f54ea512..bdd60cdf88 100644 --- a/stage0/src/Init/Lean/Elab/Frontend.lean +++ b/stage0/src/Init/Lean/Elab/Frontend.lean @@ -88,7 +88,7 @@ EIO.adaptExcept (fun (ex : Empty) => Empty.rec _ ex) $ def process (input : String) (env : Environment) (opts : Options) (fileName : Option String := none) : IO (Environment × MessageLog) := do let fileName := fileName.getD ""; let inputCtx := Parser.mkInputContext input fileName; -parserStateRef ← IO.mkRef { Parser.ModuleParserState . }; +parserStateRef ← IO.mkRef ({} : Parser.ModuleParserState); cmdStateRef ← IO.mkRef $ Command.mkState env {} opts; IO.processCommands inputCtx parserStateRef cmdStateRef; cmdState ← cmdStateRef.get; diff --git a/stage0/src/Init/Lean/Elab/Import.lean b/stage0/src/Init/Lean/Elab/Import.lean index 6c43d75af6..f862e50dd6 100644 --- a/stage0/src/Init/Lean/Elab/Import.lean +++ b/stage0/src/Init/Lean/Elab/Import.lean @@ -11,7 +11,7 @@ namespace Elab def headerToImports (header : Syntax) : List Import := let header := header.asNode; -let imports := if (header.getArg 0).isNone then [{Import . module := `Init}] else []; +let imports := if (header.getArg 0).isNone then [({ module := `Init } : Import)] else []; imports ++ (header.getArg 1).getArgs.toList.map (fun stx => -- `stx` is of the form `(Module.import "import" "runtime"? id) let runtime := !(stx.getArg 1).isNone; diff --git a/stage0/src/Init/Lean/Elab/Quotation.lean b/stage0/src/Init/Lean/Elab/Quotation.lean index 9116ff1583..37ccec4585 100644 --- a/stage0/src/Init/Lean/Elab/Quotation.lean +++ b/stage0/src/Init/Lean/Elab/Quotation.lean @@ -168,7 +168,7 @@ def HeadInfo.generalizes : HeadInfo → HeadInfo → Bool private def getHeadInfo (alt : Alt) : HeadInfo := let pat := alt.fst.head!; -let unconditional (rhsFn) := { HeadInfo . rhsFn := rhsFn }; +let unconditional (rhsFn) := ({ rhsFn := rhsFn } : HeadInfo ); -- variable pattern if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let $pat := discr; $rhs) -- wildcard pattern diff --git a/stage0/src/Init/Lean/Expr.lean b/stage0/src/Init/Lean/Expr.lean index e04f2500e5..05147d0ac7 100644 --- a/stage0/src/Init/Lean/Expr.lean +++ b/stage0/src/Init/Lean/Expr.lean @@ -79,7 +79,7 @@ protected def BinderInfo.beq : BinderInfo → BinderInfo → Bool instance BinderInfo.hasBeq : HasBeq BinderInfo := ⟨BinderInfo.beq⟩ abbrev MData := KVMap -abbrev MData.empty : MData := {KVMap .} +abbrev MData.empty : MData := ({} : KVMap) instance MVData.hasEmptc : HasEmptyc MData := ⟨MData.empty⟩ /-- diff --git a/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean b/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean index 86fbfcf7f8..43e64107fc 100644 --- a/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean +++ b/stage0/src/Init/Lean/Meta/GeneralizeTelescope.lean @@ -92,7 +92,7 @@ def generalizeTelescope {α} (es : Array Expr) (prefixForNewVars : Name) (k : Ar es ← es.mapM $ fun e => do { type ← inferType e; type ← instantiateMVars type; - pure { Entry . expr := e, type := type, modified := false } + pure { expr := e, type := type, modified := false : Entry } }; generalizeTelescopeAux prefixForNewVars k es 0 1 #[] diff --git a/stage0/src/Init/Lean/Meta/SynthInstance.lean b/stage0/src/Init/Lean/Meta/SynthInstance.lean index 7d965394cb..0bf6c7e099 100644 --- a/stage0/src/Init/Lean/Meta/SynthInstance.lean +++ b/stage0/src/Init/Lean/Meta/SynthInstance.lean @@ -362,7 +362,7 @@ answer ← withMCtx cNode.mctx $ do { val ← instantiateMVars cNode.mvar; result ← abstractMVars val; -- assignable metavariables become parameters resultType ← inferType result.expr; - pure { Answer . result := result, resultType := resultType } + pure { result := result, resultType := resultType : Answer } }; -- Remark: `answer` does not contain assignable or assigned metavariables. let key := cNode.key; @@ -465,7 +465,7 @@ traceCtx `Meta.synthInstance $ do mvar ← mkFreshExprMVar type; mctx ← getMCtx; let key := mkTableKey mctx type; - adaptState' (fun (s : Meta.State) => { State . toState := s }) (fun (s : State) => s.toState) $ do { + adaptState' (fun (s : Meta.State) => ( { toState := s } : State )) (fun (s : State) => s.toState) $ do { newSubgoal mctx key mvar Waiter.root; synth fuel } diff --git a/stage0/src/Init/Lean/Parser/Module.lean b/stage0/src/Init/Lean/Parser/Module.lean index 9fd0b1ac9f..7a679aafe2 100644 --- a/stage0/src/Init/Lean/Parser/Module.lean +++ b/stage0/src/Init/Lean/Parser/Module.lean @@ -44,7 +44,7 @@ let stx := s.stxStack.back; match s.errorMsg with | some errorMsg => let msg := mkErrorMessage ctx s.pos (toString errorMsg); - (stx, { pos := s.pos, recovering := true }, { MessageLog . }.add msg) + (stx, { pos := s.pos, recovering := true }, ({} : MessageLog).add msg) | none => (stx, { pos := s.pos }, {}) @@ -71,7 +71,7 @@ partial def parseCommand (env : Environment) (inputCtx : InputContext) : ModuleP (mkEOI pos, s, messages) else let c := mkParserContext env inputCtx; - let s := { ParserState . cache := initCacheForInput c.input, pos := pos }; + let s := { cache := initCacheForInput c.input, pos := pos : ParserState }; let s := whitespace c s; let s := (commandParser : Parser).fn c s; match s.errorMsg with diff --git a/stage0/src/Init/Lean/Parser/Parser.lean b/stage0/src/Init/Lean/Parser/Parser.lean index fd9d2252e7..81099d3c1d 100644 --- a/stage0/src/Init/Lean/Parser/Parser.lean +++ b/stage0/src/Init/Lean/Parser/Parser.lean @@ -580,7 +580,7 @@ private def rawAux (startPos : Nat) (trailingWs : Bool) : ParserFn if trailingWs then let s := whitespace c s; let stopPos' := s.pos; - let trailing := { Substring . str := input, startPos := stopPos, stopPos := stopPos' }; + let trailing := { str := input, startPos := stopPos, stopPos := stopPos' : Substring }; let atom := mkAtom { leading := leading, pos := startPos, trailing := trailing } val; s.pushSyntax atom else @@ -637,8 +637,8 @@ let leading := mkEmptySubstringAt input startPos; let val := input.extract startPos stopPos; let s := whitespace c s; let wsStopPos := s.pos; -let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos }; -let info := { SourceInfo . leading := leading, pos := startPos, trailing := trailing }; +let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }; +let info := { leading := leading, pos := startPos, trailing := trailing : SourceInfo }; s.pushSyntax (mkStxLit n val info) def charLitFnAux (startPos : Nat) : ParserFn @@ -760,7 +760,7 @@ match tk with let s := s.setPos stopPos; let s := whitespace c s; let wsStopPos := s.pos; - let trailing := { Substring . str := input, startPos := stopPos, stopPos := wsStopPos }; + let trailing := { str := input, startPos := stopPos, stopPos := wsStopPos : Substring }; let atom := mkAtom { leading := leading, pos := startPos, trailing := trailing } val; s.pushSyntax atom @@ -771,12 +771,12 @@ if isToken startPos stopPos tk then mkTokenAndFixPos startPos tk c s else let input := c.input; - let rawVal := { Substring . str := input, startPos := startPos, stopPos := stopPos }; + let rawVal := { str := input, startPos := startPos, stopPos := stopPos : Substring }; let s := whitespace c s; let trailingStopPos := s.pos; let leading := mkEmptySubstringAt input startPos; - let trailing := { Substring . str := input, startPos := stopPos, stopPos := trailingStopPos }; - let info := { SourceInfo . leading := leading, trailing := trailing, pos := startPos }; + let trailing := { str := input, startPos := stopPos, stopPos := trailingStopPos : Substring }; + let info := { leading := leading, trailing := trailing, pos := startPos : SourceInfo }; let atom := mkIdent info rawVal val; s.pushSyntax atom diff --git a/stage0/src/Init/System/FilePath.lean b/stage0/src/Init/System/FilePath.lean index 3e8fba0ed9..946cd0e4e1 100644 --- a/stage0/src/Init/System/FilePath.lean +++ b/stage0/src/Init/System/FilePath.lean @@ -49,7 +49,7 @@ def dirName (fname : String) : String := let fname := normalizePath fname; match fname.revPosOf pathSeparator with | none => "." -| some pos => { Substring . str := fname, startPos := 0, stopPos := pos }.toString +| some pos => { str := fname, startPos := 0, stopPos := pos : Substring }.toString end FilePath diff --git a/stage0/src/frontends/lean/brackets.cpp b/stage0/src/frontends/lean/brackets.cpp index b2cf3001e7..7dee425acb 100644 --- a/stage0/src/frontends/lean/brackets.cpp +++ b/stage0/src/frontends/lean/brackets.cpp @@ -82,6 +82,8 @@ static expr parse_structure_instance_core(parser & p, optional const & src p.next(); catchall = true; break; + } else if (p.curr_is_token(get_colon_tk())) { + break; } else if (!read_source) { fns.push_back(p.check_id_next("invalid structure instance, identifier expected")); p.check_token_next(get_assign_tk(), "invalid structure instance, ':=' expected"); @@ -176,6 +178,8 @@ expr parse_curly_bracket(parser & p, unsigned, expr const *, pos_info const & po return p.save_pos(mk_structure_instance(), pos); } else if (p.curr_is_token(get_dotdot_tk())) { return parse_structure_instance_core(p); + } else if (p.curr_is_token(get_colon_tk())) { + return parse_structure_instance_core(p); } else { e = p.parse_expr(); }