diff options
Diffstat (limited to '')
| -rw-r--r-- | stdlib/source/lux/type/quotient.lux | 35 | ||||
| -rw-r--r-- | stdlib/source/lux/type/refinement.lux | 36 |
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))) |