From 2e9183bc1458ededc9f5a7073e9da438573e9385 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Sun, 15 Oct 2023 16:12:43 +0200 Subject: [PATCH] add prettyDef --- lib/Quox/Definition.idr | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index 030584c..677f856 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -5,6 +5,7 @@ import public Quox.Syntax import Quox.Displace import public Data.SortedMap import public Quox.Loc +import Quox.Pretty import Control.Eff import Decidable.Decidable @@ -87,3 +88,14 @@ DefsState = StateL DEFS Definitions public export %inline lookupElim : {d, n : Nat} -> Name -> Universe -> Definitions -> Maybe (Elim d n) lookupElim x u defs = toElim !(lookup x defs) u + + +export +prettyDef : {opts : LayoutOpts} -> Name -> Definition -> Eff Pretty (Doc opts) +prettyDef name (MkDef qty type _ _) = withPrec Outer $ do + qty <- prettyQty qty.qty + dot <- dotD + name <- prettyFree name + colon <- colonD + type <- prettyTerm [<] [<] type + pure $ sep [hsep [hcat [qty, dot, name], colon], type]