add prettyDef
This commit is contained in:
parent
526aa1b3a2
commit
4678ebb625
|
@ -5,6 +5,7 @@ import public Quox.Syntax
|
||||||
import Quox.Displace
|
import Quox.Displace
|
||||||
import public Data.SortedMap
|
import public Data.SortedMap
|
||||||
import public Quox.Loc
|
import public Quox.Loc
|
||||||
|
import Quox.Pretty
|
||||||
import Control.Eff
|
import Control.Eff
|
||||||
import Decidable.Decidable
|
import Decidable.Decidable
|
||||||
|
|
||||||
|
@ -87,3 +88,22 @@ DefsState = StateL DEFS Definitions
|
||||||
public export %inline
|
public export %inline
|
||||||
lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
|
lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n)
|
||||||
lookupElim x u defs = toElim !(lookup x defs) u
|
lookupElim x u defs = toElim !(lookup x defs) u
|
||||||
|
|
||||||
|
|
||||||
|
export
|
||||||
|
prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts)
|
||||||
|
prettyDef name (MkDef qty type body _) = withPrec Outer $ do
|
||||||
|
qty <- prettyQty qty.qty
|
||||||
|
dot <- dotD
|
||||||
|
name <- prettyFree name
|
||||||
|
colon <- colonD
|
||||||
|
type <- prettyTerm [<] [<] type
|
||||||
|
case body.term0 of
|
||||||
|
Just body => do
|
||||||
|
equals <- cstD
|
||||||
|
body <- prettyTerm [<] [<] body
|
||||||
|
hangDSingle
|
||||||
|
(sep [hsep [hcat [qty, dot, name], colon], hsep [type, equals]])
|
||||||
|
body
|
||||||
|
Nothing =>
|
||||||
|
pure $ sep [hsep [hcat [qty, dot, name], colon], type]
|
||||||
|
|
Loading…
Reference in New Issue