max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Leonardo de Moura 2021-09-12 19:11:41 -07:00
parent 42436254ee
commit 20abdcb794
6 changed files with 1405 additions and 1601 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
stage0/src/Init/Conv.lean generated
View file

@ -30,7 +30,6 @@ syntax (name := change) "change " term : conv
syntax (name := delta) "delta " ident : conv
syntax (name := pattern) "pattern " term : conv
syntax (name := rewrite) "rewrite " (config)? rwRuleSeq : conv
syntax (name := erewrite) "erewrite " rwRuleSeq : conv
syntax (name := simp) "simp " ("(" &"config" " := " term ")")? (&"only ")? ("[" (simpStar <|> simpErase <|> simpLemma),* "]")? : conv
syntax (name := simpMatch) "simpMatch " : conv
@ -43,8 +42,9 @@ syntax (name := paren) "(" convSeq ")" : conv
/-- `· conv` focuses on the main conv goal and tries to solve it using `s` -/
macro dot:("·" <|> ".") s:convSeq : conv => `({%$dot ($s:convSeq) })
macro "rw " s:rwRuleSeq : conv => `(rewrite $s:rwRuleSeq)
macro "erw " s:rwRuleSeq : conv => `(erewrite $s:rwRuleSeq)
macro "rw " c:(config)? s:rwRuleSeq : conv =>
let c? := if c.isNone then none else some c[0]
`(conv| rewrite $[$c?:config]? $s:rwRuleSeq)
macro "args" : conv => `(congr)
macro "left" : conv => `(lhs)
macro "right" : conv => `(rhs)

10
stage0/src/Lean/Server/FileWorker/RequestHandling.lean generated
View file

@ -59,7 +59,7 @@ partial def handleHover (p : HoverParams)
inductive GoToKind
| declaration | definition | type
deriving DecidableEq
deriving BEq
open Elab GoToKind in
partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
@ -112,7 +112,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
if let some (ci, i) := t.hoverableInfoAt? hoverPos then
if let Info.ofTermInfo ti := i then
let mut expr := ti.expr
if kind = type then
if kind == type then
expr ← ci.runMetaM i.lctx do
Expr.getAppFn (← Meta.instantiateMVars (← Meta.inferType expr))
match expr with
@ -120,7 +120,7 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
| Expr.fvar id .. => return ← ci.runMetaM i.lctx <| locationLinksFromBinder t i id
| _ => pure ()
if let Info.ofFieldInfo fi := i then
if kind = type then
if kind == type then
let expr ← ci.runMetaM i.lctx do
Meta.instantiateMVars (← Meta.inferType fi.val)
if let some n := expr.getAppFn.constName? then
@ -129,9 +129,9 @@ partial def handleDefinition (kind : GoToKind) (p : TextDocumentPositionParams)
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i fi.projName
-- If other go-tos fail, we try to show the elaborator or parser
if let some ei := i.toElabInfo? then
if kind = declaration ∧ ci.env.contains ei.stx.getKind then
if kind == declaration && ci.env.contains ei.stx.getKind then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.stx.getKind
if kind = definition ∧ ci.env.contains ei.elaborator then
if kind == definition && ci.env.contains ei.elaborator then
return ← ci.runMetaM i.lctx <| locationLinksFromDecl i ei.elaborator
return #[]

960
stage0/stdlib/Init/Conv.c generated
View file

File diff suppressed because it is too large Load diff

501
stage0/stdlib/Lean/Elab/Deriving/DecEq.c generated
View file

File diff suppressed because one or more lines are too long

1521
stage0/stdlib/Lean/Server/FileWorker/RequestHandling.c generated
View file

File diff suppressed because it is too large Load diff

8
stage0/stdlib/Lean/Server/FileWorker/WidgetRequests.c generated
View file

@ -49,6 +49,7 @@ static lean_object* l_Lean_Widget_instInhabitedInfoPopup___closed__1;
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____closed__3;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6915____spec__22(lean_object*);
lean_object* l_Lean_Widget_TaggedText_mapM___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__13(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___lambda__5(lean_object*, lean_object*, lean_object*);
@ -115,7 +116,6 @@ lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instFromJsonRpcEncodingPacket;
static lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__5___closed__1;
extern lean_object* l_Lean_Server_rpcProcedures;
lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___spec__11(lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6979____spec__22(lean_object*);
lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__3___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____closed__1;
lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_525_(lean_object*);
@ -272,7 +272,6 @@ static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetReq
lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__14(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_821____closed__2;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_821____spec__5___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6979____spec__20(lean_object*);
static lean_object* l___private_Lean_Widget_InteractiveDiagnostic_0__Lean_Widget_Lean_MessageData_decodeUnsafe____x40_Lean_Widget_InteractiveDiagnostic___hyg_4____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__3___closed__3;
static lean_object* l___private_Lean_Widget_TaggedText_0__Lean_Widget_toJsonTaggedText____x40_Lean_Widget_TaggedText___hyg_495____at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__15___closed__3;
lean_object* l_Lean_Server_WithRpcRef_encodeUnsafe___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__12(lean_object*, lean_object*, lean_object*);
@ -289,6 +288,7 @@ lean_object* l_ExceptT_bindCont___at_Lean_Widget_Lean_Widget_InfoPopup_instRpcEn
lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__3___lambda__2(lean_object*, uint64_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__1___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6915____spec__20(lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__10___boxed__const__1;
static lean_object* l_Lean_Widget_Lean_Widget_InfoPopup_instRpcEncodingInfoPopupRpcEncodingPacket___lambda__3___closed__1;
static lean_object* l_Lean_Widget_Lean_Widget_MsgToInteractive_instRpcEncodingMsgToInteractiveRpcEncodingPacket___closed__1;
@ -8813,7 +8813,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6979____spec__20(x_3);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6915____spec__20(x_3);
x_15 = lean_alloc_closure((void*)(l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__1___boxed), 3, 1);
lean_closure_set(x_15, 0, x_14);
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__1___lambda__3___closed__1;
@ -9511,7 +9511,7 @@ lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6979____spec__22(x_3);
x_14 = l_Lean_Server_parseRequestParams___at_Lean_Server_FileWorker_initFn____x40_Lean_Server_FileWorker_RequestHandling___hyg_6915____spec__22(x_3);
x_15 = lean_alloc_closure((void*)(l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_209____spec__1___lambda__1___boxed), 3, 1);
lean_closure_set(x_15, 0, x_14);
x_16 = l_Lean_Server_registerRpcCallHandler___at_Lean_Widget_initFn____x40_Lean_Server_FileWorker_WidgetRequests___hyg_732____spec__1___lambda__3___closed__1;