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

feat: add coercions for the new frontend

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-10 13:24:13 -07:00
parent 6b7088e71a
commit 61bd10997a
1 changed files with 23 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

32
src/Lean/Message.lean
View file

@ -74,12 +74,21 @@ instance : HasAppend MessageData := ⟨compose⟩
instance : HasFormat MessageData := ⟨fun d => formatAux none d⟩
instance : HasToString MessageData := ⟨fun d => toString (format d)⟩
instance coeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance coeOfName : HasCoe Name MessageData := ⟨ofName⟩
instance coeOfSyntax : HasCoe Syntax MessageData := ⟨ofSyntax⟩
instance coeOfOptExpr : HasCoe (Option Expr) MessageData :=
instance hasCoeOfFormat : HasCoe Format MessageData := ⟨ofFormat⟩
instance hasCoeOfLevel : HasCoe Level MessageData := ⟨ofLevel⟩
instance hasCoeOfExpr : HasCoe Expr MessageData := ⟨ofExpr⟩
instance hasCoeOfName : HasCoe Name MessageData := ⟨ofName⟩
instance hasCoeOfSyntax : HasCoe Syntax MessageData := ⟨ofSyntax⟩
instance hasCoeOfOptExpr : HasCoe (Option Expr) MessageData :=
⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
instance coeOfString : Coe String MessageData := ⟨ofFormat ∘ format⟩
instance coeOfFormat : Coe Format MessageData := ⟨ofFormat⟩
instance coeOfLevel : Coe Level MessageData := ⟨ofLevel⟩
instance coeOfExpr : Coe Expr MessageData := ⟨ofExpr⟩
instance coeOfName : Coe Name MessageData := ⟨ofName⟩
instance coeOfSyntax : Coe Syntax MessageData := ⟨ofSyntax⟩
instance coeOfOptExpr : Coe (Option Expr) MessageData :=
⟨fun o => match o with | none => "none" | some e => ofExpr e⟩
partial def arrayExpr.toMessageData (es : Array Expr) : Nat → MessageData → MessageData
@ -91,7 +100,9 @@ partial def arrayExpr.toMessageData (es : Array Expr) : Nat → MessageData →
else
acc ++ "]"
instance coeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
instance hasCoeOfArrayExpr : HasCoe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
instance coeOfArrayExpr : Coe (Array Expr) MessageData := ⟨fun es => arrayExpr.toMessageData es 0 "#["⟩
def bracket (l : String) (f : MessageData) (r : String) : MessageData := group (nest l.length $ l ++ f ++ r)
def paren (f : MessageData) : MessageData := bracket "(" f ")"
@ -106,8 +117,11 @@ def ofList: List MessageData → MessageData
def ofArray (msgs : Array MessageData) : MessageData :=
ofList msgs.toList
instance coeOfList : HasCoe (List MessageData) MessageData := ⟨ofList⟩
instance coeOfListExpr : HasCoe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
instance hasCoeOfList : HasCoe (List MessageData) MessageData := ⟨ofList⟩
instance hasCoeOfListExpr : HasCoe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
instance coeOfList : Coe (List MessageData) MessageData := ⟨ofList⟩
instance coeOfListExpr : Coe (List Expr) MessageData := ⟨fun es => ofList $ es.map ofExpr⟩
end MessageData