aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2019-03-12 23:31:05 -0400
committerEduardo Julian2019-03-12 23:31:05 -0400
commit54d28f88a4293513621bd8ce5c26e3e6e74f345b (patch)
treed386de3338a97f5b93921606e8d2f23366c71423
parentfafed063904d6ca7bfa3d9c4ba4b8d44e7b97549 (diff)
Re-defined the "type" macros in terms of ":by-example".
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux/type/quotient.lux35
-rw-r--r--stdlib/source/lux/type/refinement.lux36
2 files changed, 15 insertions, 56 deletions
diff --git a/stdlib/source/lux/type/quotient.lux b/stdlib/source/lux/type/quotient.lux
index 7d56a1b24..b5efe0957 100644
--- a/stdlib/source/lux/type/quotient.lux
+++ b/stdlib/source/lux/type/quotient.lux
@@ -1,15 +1,7 @@
(.module:
[lux (#- type)
- [control
- [monad (#+ do)]
- ["p" parser]]
- [data
- ["." error (#+ Error)]]
- ["." type
- abstract]
- ["." macro
- ["s" syntax (#+ syntax:)]
- ["." poly]]])
+ [type (#+ :by-example)
+ abstract]])
(abstract: #export (Class t c q)
{}
@@ -46,21 +38,8 @@
)
)
-(def: (quotient-type constructor-type)
- (-> Type (Error Type))
- (<| (poly.run constructor-type)
- (do p.monad
- [[valueT classT quotient-ex] (<| poly.apply (p.after (poly.exactly ..Class))
- ($_ p.and poly.any poly.any poly.existential))]
- (wrap (.type (..Quotient valueT classT (:~ (#.Ex quotient-ex))))))))
-
-(syntax: #export (type {quotient s.identifier})
- (do @
- [constructorT (macro.find-type quotient)
- quotientT (case (quotient-type constructorT)
- (#error.Success quotientT)
- (wrap quotientT)
-
- (#error.Failure error)
- (p.fail error))]
- (wrap (list (type.to-code quotientT)))))
+(template: #export (type <class>)
+ (:by-example [t c q]
+ {(..Class t c q)
+ <class>}
+ (..Quotient t c q)))
diff --git a/stdlib/source/lux/type/refinement.lux b/stdlib/source/lux/type/refinement.lux
index 0881eb8eb..142f77b0e 100644
--- a/stdlib/source/lux/type/refinement.lux
+++ b/stdlib/source/lux/type/refinement.lux
@@ -1,16 +1,9 @@
(.module:
[lux (#- type)
[control
- [predicate (#+ Predicate)]
- [monad (#+ do)]
- ["p" parser]]
- [data
- ["." error (#+ Error)]]
- ["." type ("#/." equivalence)
- abstract]
- ["." macro
- ["s" syntax (#+ syntax:)]
- ["." poly]]])
+ [predicate (#+ Predicate)]]
+ [type (#+ :by-example) ("#/." equivalence)
+ abstract]])
(abstract: #export (Refined t r)
{#.doc "A refined type 'r' of base type 't' using a predicate."}
@@ -84,21 +77,8 @@
[yes
(#.Cons head no)]))))
-(def: (refinement-type constructor-type)
- (-> Type (Error Type))
- (<| (poly.run constructor-type)
- (do p.monad
- [[un-refinedT refined-ex] (poly.apply (p.after (poly.exactly ..Refiner)
- (p.and poly.any poly.existential)))]
- (wrap (.type (..Refined un-refinedT (#.Ex refined-ex)))))))
-
-(syntax: #export (type {refinement s.identifier})
- (do @
- [constructorT (macro.find-type refinement)
- refinementT (case (refinement-type constructorT)
- (#error.Success refinementT)
- (wrap refinementT)
-
- (#error.Failure error)
- (p.fail error))]
- (wrap (list (type.to-code refinementT)))))
+(template: #export (type <refiner>)
+ (:by-example [t r]
+ {(..Refiner t r)
+ <refiner>}
+ (..Refined t r)))