From 103f019dbdf1236148d9e5b99286df0b003769ac Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Mon, 27 Nov 2023 07:37:38 +0100 Subject: [PATCH] move NDefinition to Quox.Definition and add an untyped one --- lib/Quox/Definition.idr | 6 +++++- lib/Quox/Parser/FromParser.idr | 5 ----- lib/Quox/Untyped/Syntax.idr | 4 ++++ 3 files changed, 9 insertions(+), 6 deletions(-) diff --git a/lib/Quox/Definition.idr b/lib/Quox/Definition.idr index 1fc19aa..900536d 100644 --- a/lib/Quox/Definition.idr +++ b/lib/Quox/Definition.idr @@ -89,12 +89,16 @@ isZero g = g.qty == GZero public export -data DefEnvTag = DEFS +NDefinition : Type +NDefinition = (Name, Definition) public export Definitions : Type Definitions = SortedMap Name Definition +public export +data DefEnvTag = DEFS + public export DefsReader : Type -> Type DefsReader = ReaderL DEFS Definitions diff --git a/lib/Quox/Parser/FromParser.idr b/lib/Quox/Parser/FromParser.idr index 5907663..42b8d57 100644 --- a/lib/Quox/Parser/FromParser.idr +++ b/lib/Quox/Parser/FromParser.idr @@ -27,11 +27,6 @@ import Data.IORef %default total -public export -NDefinition : Type -NDefinition = (Name, Definition) - - public export data StateTag = NS | SEEN diff --git a/lib/Quox/Untyped/Syntax.idr b/lib/Quox/Untyped/Syntax.idr index 918aa61..bed1927 100644 --- a/lib/Quox/Untyped/Syntax.idr +++ b/lib/Quox/Untyped/Syntax.idr @@ -93,6 +93,10 @@ public export 0 Definitions : Type Definitions = SortedMap Name Definition +public export +0 NDefinition : Type +NDefinition = (Name, Definition) + export covering prettyTerm : {opts : LayoutOpts} -> BContext n ->