From a4c4a5b8c744eae8108c02e402600a61fdc74d02 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Mon, 25 Dec 2017 00:24:18 -0400 Subject: - Added module for predicates. - Added refinement types. - Small refactorings and fixes. - Added the capacity to unquote expressions inside the 'lux.type' macro. --- stdlib/source/lux.lux | 3 ++ stdlib/source/lux/control/predicate.lux | 37 ++++++++++++++++ stdlib/source/lux/lang/type.lux | 20 ++++----- stdlib/source/lux/macro/poly.lux | 38 +++++++++++------ stdlib/source/lux/macro/poly/eq.lux | 4 +- stdlib/source/lux/macro/poly/functor.lux | 4 +- stdlib/source/lux/macro/poly/json.lux | 8 ++-- stdlib/source/lux/type/refinement.lux | 72 ++++++++++++++++++++++++++++++++ stdlib/test/test/lux/math/modular.lux | 2 +- stdlib/test/tests.lux | 6 ++- 10 files changed, 158 insertions(+), 36 deletions(-) create mode 100644 stdlib/source/lux/control/predicate.lux create mode 100644 stdlib/source/lux/type/refinement.lux (limited to 'stdlib') diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux index cf5707996..e4214a899 100644 --- a/stdlib/source/lux.lux +++ b/stdlib/source/lux.lux @@ -2608,6 +2608,9 @@ #Nil))))] (` ("lux in-module" (~ (text$ module)) (~ (walk-type type')))) + [_ (#Form (#Cons [_ (#Symbol ["" "~"])] (#Cons expression #Nil)))] + expression + [_ (#Form (#Cons type-fn args))] (list/fold ("lux check" (-> Code Code Code) (function' [arg type-fn] (` (#.Apply (~ arg) (~ type-fn))))) diff --git a/stdlib/source/lux/control/predicate.lux b/stdlib/source/lux/control/predicate.lux new file mode 100644 index 000000000..f4ca17d70 --- /dev/null +++ b/stdlib/source/lux/control/predicate.lux @@ -0,0 +1,37 @@ +(.module: + lux + (lux (data (coll [set #+ Set])))) + +(type: #export (Pred a) + (-> a Bool)) + +(do-template [ ] + [(def: #export ( left right) + (All [a] (-> (Pred a) (Pred a) (Pred a))) + (function [value] + ( (left value) + (right value))))] + + [union or] + [intersection and] + ) + +(def: #export (complement predicate) + (All [a] (-> (Pred a) (Pred a))) + (|>> predicate not)) + +(def: #export (difference sub base) + (All [a] (-> (Pred a) (Pred a) (Pred a))) + (function [value] + (and (base value) + (not (sub value))))) + +(def: #export (set set) + (All [a] (-> (Set a) (Pred a))) + (set.member? set)) + +(def: #export (rec predicate) + (All [a] + (-> (-> (Pred a) (Pred a)) + (Pred a))) + (|>> (predicate (rec predicate)))) diff --git a/stdlib/source/lux/lang/type.lux b/stdlib/source/lux/lang/type.lux index 43febdb8c..33cb2a033 100644 --- a/stdlib/source/lux/lang/type.lux +++ b/stdlib/source/lux/lang/type.lux @@ -164,12 +164,12 @@ _ #.None))) -(def: #export (to-ast type) +(def: #export (to-code type) (-> Type Code) (case type (#.Primitive name params) (` (#.Primitive (~ (code.text name)) - (list (~+ (list/map to-ast params))))) + (.list (~+ (list/map to-code params))))) (^template [] @@ -183,23 +183,17 @@ (^template [] ( left right) - (` ( (~ (to-ast left)) - (~ (to-ast right))))) - ([#.Function] [#.Apply]) - - (^template [ ] - ( left right) - (` ( (~+ (list/map to-ast ( type)))))) - ([#.Sum | flatten-variant] - [#.Product & flatten-tuple]) + (` ( (~ (to-code left)) + (~ (to-code right))))) + ([#.Sum] [#.Product] [#.Function] [#.Apply]) (#.Named name sub-type) (code.symbol name) (^template [] ( env body) - (` ( (list (~+ (list/map to-ast env))) - (~ (to-ast body))))) + (` ( (.list (~+ (list/map to-code env))) + (~ (to-code body))))) ([#.UnivQ] [#.ExQ]) )) diff --git a/stdlib/source/lux/macro/poly.lux b/stdlib/source/lux/macro/poly.lux index a14e415b4..a84196f2c 100644 --- a/stdlib/source/lux/macro/poly.lux +++ b/stdlib/source/lux/macro/poly.lux @@ -2,7 +2,8 @@ [lux #- function] (lux (control [monad #+ do Monad] [eq] - ["p" parser]) + ["p" parser] + ["ex" exception #+ exception:]) [function] (data [text "text/" Monoid] (coll [list "list/" Fold Monad Monoid] @@ -260,8 +261,8 @@ (case headT (#.Bound idx) (case (dict.get (adjusted-idx env idx) env) - (#.Some [poly-type poly-ast]) - (wrap poly-ast) + (#.Some [poly-type poly-code]) + (wrap poly-code) #.None (p.fail ($_ text/compose "Unknown bound type: " (type.to-text headT)))) @@ -285,6 +286,19 @@ _ (p.fail ($_ text/compose "Not a bound type: " (type.to-text headT)))))) +(exception: #export Not-Existential-Type) + +(def: #export existential + (Poly Nat) + (do p.Monad + [headT any] + (case headT + (#.Ex ex-id) + (wrap ex-id) + + _ + (p.fail (Not-Existential-Type (type.to-text headT)))))) + (def: #export named (Poly [Ident Type]) (do p.Monad @@ -407,12 +421,12 @@ (~ impl))))))) ## [Derivers] -(def: #export (to-ast env type) +(def: #export (to-code env type) (-> Env Type Code) (case type (#.Primitive name params) (` (#.Primitive (~ (code.text name)) - (list (~+ (list/map (to-ast env) params))))) + (list (~+ (list/map (to-code env) params))))) (^template [] @@ -427,24 +441,24 @@ (#.Bound idx) (let [idx (adjusted-idx env idx)] (if (n/= +0 idx) - (|> (dict.get idx env) maybe.assume product.left (to-ast env)) + (|> (dict.get idx env) maybe.assume product.left (to-code env)) (` (.$ (~ (code.nat (n/dec idx))))))) (#.Apply #.Void (#.Bound idx)) (let [idx (adjusted-idx env idx)] (if (n/= +0 idx) - (|> (dict.get idx env) maybe.assume product.left (to-ast env)) + (|> (dict.get idx env) maybe.assume product.left (to-code env)) (undefined))) (^template [] ( left right) - (` ( (~ (to-ast env left)) - (~ (to-ast env right))))) + (` ( (~ (to-code env left)) + (~ (to-code env right))))) ([#.Function] [#.Apply]) (^template [ ] ( left right) - (` ( (~+ (list/map (to-ast env) ( type)))))) + (` ( (~+ (list/map (to-code env) ( type)))))) ([#.Sum | type.flatten-variant] [#.Product & type.flatten-tuple]) @@ -453,7 +467,7 @@ (^template [] ( scope body) - (` ( (list (~+ (list/map (to-ast env) scope))) - (~ (to-ast env body))))) + (` ( (list (~+ (list/map (to-code env) scope))) + (~ (to-code env body))))) ([#.UnivQ] [#.ExQ]) )) diff --git a/stdlib/source/lux/macro/poly/eq.lux b/stdlib/source/lux/macro/poly/eq.lux index 3550df0c0..1da35d91e 100644 --- a/stdlib/source/lux/macro/poly/eq.lux +++ b/stdlib/source/lux/macro/poly/eq.lux @@ -36,7 +36,7 @@ inputT poly.peek #let [@Eq (: (-> Type Code) (function [type] - (` (eq.Eq (~ (poly.to-ast *env* type))))))]] + (` (eq.Eq (~ (poly.to-code *env* type))))))]] ($_ p.either ## Basic types (~~ (do-template [ ] @@ -136,7 +136,7 @@ [[funcC varsC bodyC] (poly.polymorphic Eq)] (wrap (` (: (All [(~+ varsC)] (-> (~+ (list/map (|>> (~) eq.Eq (`)) varsC)) - (eq.Eq ((~ (poly.to-ast *env* inputT)) (~+ varsC))))) + (eq.Eq ((~ (poly.to-code *env* inputT)) (~+ varsC))))) (function (~ funcC) [(~+ varsC)] (~ bodyC)))))) poly.recursive-call diff --git a/stdlib/source/lux/macro/poly/functor.lux b/stdlib/source/lux/macro/poly/functor.lux index 79740c32c..f3ed46041 100644 --- a/stdlib/source/lux/macro/poly/functor.lux +++ b/stdlib/source/lux/macro/poly/functor.lux @@ -28,10 +28,10 @@ #let [@Functor (: (-> Type Code) (function [unwrappedT] (if (n/= +1 num-vars) - (` (functor.Functor (~ (poly.to-ast *env* unwrappedT)))) + (` (functor.Functor (~ (poly.to-code *env* unwrappedT)))) (let [paramsC (|> num-vars n/dec list.indices (L/map (|>> %n code.local-symbol)))] (` (All [(~+ paramsC)] - (functor.Functor ((~ (poly.to-ast *env* unwrappedT)) (~+ paramsC))))))))) + (functor.Functor ((~ (poly.to-code *env* unwrappedT)) (~+ paramsC))))))))) Arg (: (-> Code (poly.Poly Code)) (function Arg [valueC] ($_ p.either diff --git a/stdlib/source/lux/macro/poly/json.lux b/stdlib/source/lux/macro/poly/json.lux index 155042437..9a3096dff 100644 --- a/stdlib/source/lux/macro/poly/json.lux +++ b/stdlib/source/lux/macro/poly/json.lux @@ -105,7 +105,7 @@ [*env* poly.env #let [@JSON//encode (: (-> Type Code) (function [type] - (` (-> (~ (poly.to-ast *env* type)) //.JSON))))] + (` (-> (~ (poly.to-code *env* type)) //.JSON))))] inputT poly.peek] ($_ p.either @@ -178,7 +178,7 @@ (wrap (` (: (All [(~+ varsC)] (-> (~+ (list/map (function [varC] (` (-> (~ varC) //.JSON))) varsC)) - (-> ((~ (poly.to-ast *env* inputT)) (~+ varsC)) + (-> ((~ (poly.to-code *env* inputT)) (~+ varsC)) //.JSON))) (function (~ funcC) [(~+ varsC)] (~ bodyC)))))) @@ -217,7 +217,7 @@ [*env* poly.env #let [@JSON//decode (: (-> Type Code) (function [type] - (` (//.Reader (~ (poly.to-ast *env* type))))))] + (` (//.Reader (~ (poly.to-code *env* type))))))] inputT poly.peek] ($_ p.either @@ -273,7 +273,7 @@ [[funcC varsC bodyC] (poly.polymorphic Codec//decode)] (wrap (` (: (All [(~+ varsC)] (-> (~+ (list/map (|>> (~) //.Reader (`)) varsC)) - (//.Reader ((~ (poly.to-ast *env* inputT)) (~+ varsC))))) + (//.Reader ((~ (poly.to-code *env* inputT)) (~+ varsC))))) (function (~ funcC) [(~+ varsC)] (~ bodyC)))))) poly.bound diff --git a/stdlib/source/lux/type/refinement.lux b/stdlib/source/lux/type/refinement.lux new file mode 100644 index 000000000..55aa3cdd7 --- /dev/null +++ b/stdlib/source/lux/type/refinement.lux @@ -0,0 +1,72 @@ +(.module: + [lux #- Ref type] + (lux (control [predicate #+ Pred] + [monad #+ do] + ["p" parser]) + (data ["e" error #+ Error]) + (lang [type "type/" Eq]) + (type abstract) + [macro] + (macro ["s" syntax #+ syntax:] + [poly]))) + +(abstract: #export (Ref t r) + {#.doc "A refinement 'r' on type 't' based on a predicate."} + + {#value t + #predicate (Pred t)} + + (def: #export (refinement predicate) + (All [t] + (Ex [r] + (-> (Pred t) (-> t (Maybe (Ref t r)))))) + (function [un-refined] + (if (predicate un-refined) + (#.Some (@abstraction {#value un-refined + #predicate predicate})) + #.None))) + + (do-template [ ] + [(def: #export ( refined) + (All [t r] (-> (Ref t r) )) + (|> refined @representation (get@ )))] + + [un-refine t #value] + [predicate (Pred t) #predicate] + ) + + (def: #export (lift transform) + (All [t r] + (-> (-> t t) + (-> (Ref t r) (Maybe (Ref t r))))) + (function [refined] + (let [[value predicate] (@representation refined) + value' (transform value)] + (if (predicate value') + (#.Some (@abstraction {#value value' + #predicate predicate})) + #.None)))) + ) + +(def: (refinement-type constructor-type) + (-> Type (Error Type)) + (<| (poly.run constructor-type) + (do p.Monad + [[un-refinedT outputT] (poly.function poly.any poly.any) + refined-ex (<| (poly.local (list outputT)) + poly.apply (p.after (poly.this .Maybe)) + poly.apply (p.after (poly.this ..Ref)) + (p.after (poly.this un-refinedT)) + poly.existential)] + (wrap (.type (..Ref un-refinedT (#.Ex refined-ex))))))) + +(syntax: #export (type [refinement s.symbol]) + (do @ + [constructorT (macro.find-type refinement) + refinementT (case (refinement-type constructorT) + (#e.Success refinementT) + (wrap refinementT) + + (#e.Error error) + (p.fail error))] + (wrap (list (type.to-code refinementT))))) diff --git a/stdlib/test/test/lux/math/modular.lux b/stdlib/test/test/lux/math/modular.lux index 76d56cbc2..1adc737a4 100644 --- a/stdlib/test/test/lux/math/modular.lux +++ b/stdlib/test/test/lux/math/modular.lux @@ -11,7 +11,7 @@ lux/test) (def: %3 (/.modulus 3)) -(def: Mod3 Type (type-of %3)) +(type: Mod3 (~ (type-of %3))) (def: modulusR (r.Random Int) diff --git a/stdlib/test/tests.lux b/stdlib/test/tests.lux index 1742334d8..12ab83fc0 100644 --- a/stdlib/test/tests.lux +++ b/stdlib/test/tests.lux @@ -74,7 +74,8 @@ ["_." udp])) )) (lux (control [contract] - [concatenative]) + [concatenative] + [predicate]) (data [env] [trace] [store] @@ -85,7 +86,8 @@ (coll (tree ["tree_." parser]))) [macro] (macro (poly [json])) - (type [unit]) + (type [unit] + [refinement]) [world/env] [world/console]) ) -- cgit v1.2.3