diff --git a/stdlib/source/library/lux/function.lux b/stdlib/source/library/lux/function.lux index cc115a51b..cc9221a26 100644 --- a/stdlib/source/library/lux/function.lux +++ b/stdlib/source/library/lux/function.lux @@ -46,7 +46,7 @@ (-> cause effect)) -(the .public pro_functor +(the .public functor (pro.Functor Function) (implementation (the (each before after it) diff --git a/stdlib/source/library/lux/optic.lux b/stdlib/source/library/lux/optic.lux index 0f9bf89a1..527e72d52 100644 --- a/stdlib/source/library/lux/optic.lux +++ b/stdlib/source/library/lux/optic.lux @@ -25,124 +25,223 @@ (<| (.in_module# .prelude) .with_template)) -(the Its - (macro (_ focus focus' context context') - [(-> context - focus)])) - -(the Has - (macro (_ focus focus' context context') - [(-> [focus' context] - context')])) - -(every .public (Lens focus focus' context context') - (Record - [#its (Its focus focus' context context') - #has (Has focus focus' context context')])) - -(the .public (lens its has) - (for_any (_ focus focus' context context') - (-> (Its focus focus' context context') (Has focus focus' context context') - (Lens focus focus' context context'))) - [#its its - #has has]) - -(the .public its - (for_any (_ focus focus' context context') - (-> (Lens focus focus' context context') - (Its focus focus' context context'))) - (.its #its)) - -(the .public (has lens value context) - (for_any (_ focus focus' context context') - (-> (Lens focus focus' context context') - (-> focus' - (-> context context')))) - (by lens #has [value context])) - -(the .public (revised lens change context) - (for_any (_ focus focus' context context') - (-> (Lens focus focus' context context') - (-> (-> focus focus') - (-> context context')))) - (by lens #has [(change (its lens context)) context])) +(every .public (Optic it internal_cause internal_effect external_cause external_effect) + (-> (it internal_cause internal_effect) + (it external_cause external_effect))) + +(these (every .public (View internal_cause internal_effect external_cause external_effect) + (for_any (_ it) + (-> (pro.Functor it) + (Optic it internal_cause internal_effect external_cause external_effect)))) + + (the As + (macro (_ internal_cause internal_effect external_cause external_effect) + [(-> internal_effect + external_effect)])) + + (the Of + (macro (_ internal_cause internal_effect external_cause external_effect) + [(-> external_cause + internal_cause)])) + + (every .public (View' internal_cause internal_effect external_cause external_effect) + (Record + [#as (As internal_cause internal_effect external_cause external_effect) + #of (Of internal_cause internal_effect external_cause external_effect)])) + + (the .public (view' as of) + (for_any (_ internal_cause internal_effect external_cause external_effect) + (-> (As internal_cause internal_effect external_cause external_effect) (Of internal_cause internal_effect external_cause external_effect) + (View' internal_cause internal_effect external_cause external_effect))) + [#as as + #of of]) + + (the functor_of_view + (for_any (_ internal_cause internal_effect) + (pro.Functor (View' internal_cause internal_effect))) + (implementation + (the (each before after [/#as /#of]) + (..view' (|>> /#as after) + (|>> before /#of))))) + + (with_template [,name ,type ,tag] + [(the .public ,name + (for_any (_ internal_cause internal_effect external_cause external_effect) + (-> (View' internal_cause internal_effect external_cause external_effect) + (,type internal_cause internal_effect external_cause external_effect))) + (.its ,tag))] + + [as As #as] + [of Of #of] + ) + + (the (as_view [/#as /#of] + [pro_functor]) + (for_any (_ internal_cause internal_effect external_cause external_effect) + (-> (View' internal_cause internal_effect external_cause external_effect) + (View internal_cause internal_effect external_cause external_effect))) + (<| (.with pro_functor) + (each /#of /#as))) + + (the identity_view' + (for_any (_ internal_cause internal_effect) + (View' internal_cause internal_effect + internal_cause internal_effect)) + (view' function.identity function.identity)) + + (the (as_view' it) + (for_any (_ internal_cause internal_effect external_cause external_effect) + (-> (View internal_cause internal_effect external_cause external_effect (View' internal_cause internal_effect)) + (View' internal_cause internal_effect external_cause external_effect))) + (it [..functor_of_view] + ..identity_view')) + ) + +(these (every .public (Property internal_cause internal_effect external_cause external_effect) + (for_any (_ it) + (-> [(pro.Functor it) (pro.Cartesian it)] + (Optic it internal_cause internal_effect external_cause external_effect)))) + + (the Its + (macro (_ focus focus' context context') + [(-> context + focus)])) + + (the Has + (macro (_ focus focus' context context') + [(-> [focus' context] + context')])) + + (every .public (Property' focus focus' context context') + (Record + [#its (Its focus focus' context context') + #has (Has focus focus' context context')])) + + (the .public (property' its has) + (for_any (_ focus focus' context context') + (-> (Its focus focus' context context') (Has focus focus' context context') + (Property' focus focus' context context'))) + [#its its + #has has]) + + (the functor_of_property' + (for_any (_ internal_cause internal_effect) + (pro.Functor (Property' internal_cause internal_effect))) + (implementation + (the (each before after [/#its /#has]) + (..property' (|>> before + /#its) + (|>> (product.then function.identity before) + /#has + after))))) + + (the cartesian_of_property' + (for_any (_ internal_cause internal_effect) + (pro.Cartesian (Property' internal_cause internal_effect))) + (implementation + (the (in_left [/#its /#has]) + (..property' (|>> product.left + /#its) + (product.forked (|>> (product.then function.identity product.left) + /#has) + (|>> product.right + product.right)))) + (the (in_right [/#its /#has]) + (..property' (|>> product.right + /#its) + (product.forked (|>> product.right + product.left) + (|>> (product.then function.identity product.right) + /#has)))))) + + (the .public (as_property [/#its /#has] + [pro_functor cartesian]) + (for_any (_ internal_cause internal_effect external_cause external_effect) + (-> (Property' internal_cause internal_effect external_cause external_effect) + (Property internal_cause internal_effect external_cause external_effect))) + (<| (.with pro_functor) + (.with cartesian) + (|>> in_left + (each (product.forked /#its function.identity) /#has)))) + + (the identity_property' + (for_any (_ internal_cause internal_effect) + (Property' internal_cause internal_effect + internal_cause internal_effect)) + (..property' function.identity product.left)) + + (the .public (as_property' it) + (for_any (_ internal_cause internal_effect external_cause external_effect) + (-> (Property internal_cause internal_effect external_cause external_effect (Property' internal_cause internal_effect)) + (Property' internal_cause internal_effect external_cause external_effect))) + (it [..functor_of_property' ..cartesian_of_property'] + ..identity_property')) + + (the .public its + (for_any (_ focus focus' context context') + (-> (Property' focus focus' context context') + (Its focus focus' context context'))) + (.its #its)) + + (the .public (has property' value context) + (for_any (_ focus focus' context context') + (-> (Property' focus focus' context context') + (-> focus' + (-> context context')))) + (by property' #has [value context])) + + (the .public (revised property' change context) + (for_any (_ focus focus' context context') + (-> (Property' focus focus' context context') + (-> (-> focus focus') + (-> context context')))) + (by property' #has [(change (its property' context)) context])) + ) (the .public (composite outer inner) (for_any (_ focus focus' middle middle' context context') - (-> (Lens middle middle' context context') (Lens focus focus' middle middle') - (Lens focus focus' context context'))) + (-> (Property' middle middle' context context') (Property' focus focus' middle middle') + (Property' focus focus' context context'))) [#its (|>> (its outer) (its inner)) #has (function (_ [focus context]) (revised outer (has inner focus) context))]) -(the As - (macro (_ it alternative) - [(-> it - alternative)])) - -(the Of - (macro (_ it alternative) - [(-> alternative - it)])) - -(every .public (View it alternative) - (Record - [#as (As it alternative) - #of (Of it alternative)])) - -(the .public (view as of) - (for_any (_ it alternative) - (-> (As it alternative) (Of it alternative) - (View it alternative))) - [#as as - #of of]) - -(with_template [,name ,type ,tag] - [(the .public ,name - (for_any (_ it alternative) - (-> (View it alternative) - (,type it alternative))) - (.its ,tag))] - - [as As #as] - [of Of #of] - ) - -(the When - (macro (_ context case) - [(-> context - (Or context case))])) - -(the Some - (macro (_ context case) - [(-> case - context)])) - -(every .public (Prism context case) - (Record - [#when (When context case) - #some (Some context case)])) - -(the .public (prism when some) - (for_any (_ context case) - (-> (When context case) (Some context case) - (Prism context case))) - [#when when - #some some]) - -(with_template [,name ,type ,tag] - [(the .public ,name - (for_any (_ context case) - (-> (Prism context case) - (,type context case))) - (.its ,tag))] - - [when When #when] - [some Some #some] - ) +(these (the When + (macro (_ context case) + [(-> context + (Or context case))])) + + (the Some + (macro (_ context case) + [(-> case + context)])) + + (every .public (Case context case) + (Record + [#when (When context case) + #some (Some context case)])) + + (the .public (case when some) + (for_any (_ context case) + (-> (When context case) (Some context case) + (Case context case))) + [#when when + #some some]) + + (with_template [,name ,type ,tag] + [(the .public ,name + (for_any (_ context case) + (-> (Case context case) + (,type context case))) + (.its ,tag))] + + [when When #when] + [some Some #some] + ) + ) ... TODO: Make this nominal type unnecessary. (nominal.every .public (Membership one all) @@ -171,7 +270,7 @@ (.when (nominal.reification it) {#All all} {#All (value all)} - + {#One one next} {#One one (each (function (_ before) (|>> before @@ -199,15 +298,15 @@ (implementation (the functor ..membership_functor) (the pure (|>> {#All} nominal.abstraction)) - (the (with effect cause) - (.when (nominal.reification effect) - {#All effect} - (by ..membership_functor each effect cause) - - {#One one effect} + (the (with internal_effect internal_cause) + (.when (nominal.reification internal_effect) + {#All internal_effect} + (by ..membership_functor each internal_effect internal_cause) + + {#One one internal_effect} (nominal.abstraction - {#One one (with (by ..membership_functor each function.flipped effect) - cause)}))))) + {#One one (with (by ..membership_functor each function.flipped internal_effect) + internal_cause)}))))) (the .public (one it) (for_any (_ it) @@ -222,67 +321,11 @@ (.when (nominal.reification it) {#All it} it - + {#One one next} - ((all next) one)) - )) - -(every .public (Member all one) - (-> all - (Membership one all))) - -(every .public (Optic it cause effect cause' effect') - (-> (it cause effect) - (it cause' effect'))) - -(every .public (Property cause effect cause' effect') - (for_any (_ it) - (-> [(pro.Functor it) (pro.Cartesian it)] - (Optic it cause effect cause' effect')))) - -(the .public pro_functor_of_lens - (for_any (_ cause effect) - (pro.Functor (Lens cause effect))) - (implementation - (the (each before after [/#its /#has]) - (..lens (|>> before - /#its) - (|>> (product.then function.identity before) - /#has - after))))) - -(the .public cartesian_of_lens - (for_any (_ cause effect) - (pro.Cartesian (Lens cause effect))) - (implementation - (the (in_left [/#its /#has]) - (..lens (|>> product.left - /#its) - (product.forked (|>> (product.then function.identity product.left) - /#has) - (|>> product.right - product.right)))) - (the (in_right [/#its /#has]) - (..lens (|>> product.right - /#its) - (product.forked (|>> product.right - product.left) - (|>> (product.then function.identity product.right) - /#has)))))) - -(the .public (as_property [/#its /#has] - [pro_functor cartesian]) - (for_any (_ cause effect cause' effect') - (-> (Lens cause effect cause' effect') - (Property cause effect cause' effect'))) - (<| (.with pro_functor) - (.with cartesian) - (|>> in_left - (each (product.forked /#its function.identity) /#has)))) - -(the .public (as_lens it) - (for_any (_ cause effect cause' effect') - (-> (Property cause effect cause' effect' (Lens cause effect)) - (Lens cause effect cause' effect'))) - (it [..pro_functor_of_lens ..cartesian_of_lens] - (..lens function.identity product.left))) + ((all next) one))) + + (every .public (Member all one) + (-> all + (Membership one all))) + ) diff --git a/stdlib/source/test/lux/optic.lux b/stdlib/source/test/lux/optic.lux index 7bcdc4f4f..f2879ed74 100644 --- a/stdlib/source/test/lux/optic.lux +++ b/stdlib/source/test/lux/optic.lux @@ -26,29 +26,29 @@ ["[0]" /]]) (the sign - (/.Lens Bit Bit - Integer Integer) - (/.lens (integer.>= +0) - (function (has [sign mantissa]) - ((is (Change Integer) - (if sign - function.identity - integer.opposite)) - (integer.absolute mantissa))))) + (/.Property' Bit Bit + Integer Integer) + (/.property' (integer.>= +0) + (function (has [sign mantissa]) + ((is (Change Integer) + (if sign + function.identity + integer.opposite)) + (integer.absolute mantissa))))) (the left (for_any (_ left right) - (/.Lens left left - [left right] [left right])) - (/.lens product.left - (function (has [left [_ right]]) - [left right]))) + (/.Property' left left + [left right] [left right])) + (/.property' product.left + (function (has [left [_ right]]) + [left right]))) -(the .public (lens_specification it - equivalence_of_context equivalence_of_focus - random_context random_focus) +(the .public (property'_specification it + equivalence_of_context equivalence_of_focus + random_context random_focus) (for_any (_ focus context) - (-> (/.Lens focus focus context context) + (-> (/.Property' focus focus context context) (Equivalence context) (Equivalence focus) (Random context) (Random focus) Test)) @@ -56,7 +56,7 @@ [expected_context random_context expected_focus random_focus other_focus random_focus] - (<| (_.for [/.Lens /.lens]) + (<| (_.for [/.Property' /.property']) (all _.and (_.coverage [/.#has /.has] (let [later_writes_overwrite_earlier_writes! @@ -82,7 +82,7 @@ equivalence_of_it equivalence_of_alternative random_it random_alternative) (for_any (_ it alternative) - (-> (/.View it alternative) + (-> (/.View' it it alternative alternative) (Equivalence it) (Equivalence alternative) (Random it) (Random alternative) Test)) @@ -92,7 +92,7 @@ alternative_0 random_alternative alternative_1 random_alternative] - (<| (_.for [/.View /.view]) + (<| (_.for [/.View' /.view']) (all _.and (_.coverage [/.#as /.as] (and (bit.= (by equivalence_of_it = it_0 it_1) @@ -112,33 +112,34 @@ (the list_as_stack (for_any (_ it) - (/.View (List it) (Stack it))) - (/.view list.as_stack - list.of_stack)) + (/.View' (List it) (List it) + (Stack it) (Stack it))) + (/.view' list.as_stack + list.of_stack)) -(the .public (prism_specification prism - equivalence_of_context equivalence_of_case - random_context random_case) +(the .public (case_specification case + equivalence_of_context equivalence_of_case + random_context random_case) (for_any (_ context case) - (-> (/.Prism context case) + (-> (/.Case context case) (Equivalence context) (Equivalence case) (Random context) (Random case) Test)) (do [! random.monad] [expected_context random_context expected_case random_case] - (<| (_.for [/.Prism /.prism]) + (<| (_.for [/.Case /.case]) (all _.and (_.coverage [/.#when /.when] - (when (/.when prism expected_context) + (when (/.when case expected_context) {.#Left actual_context} (same? expected_context actual_context) {.#Right actual_case} - (by equivalence_of_context = expected_context (/.some prism actual_case)))) + (by equivalence_of_context = expected_context (/.some case actual_case)))) (_.coverage [/.#some /.some] - (let [expected_context (/.some prism expected_case)] - (when (/.when prism expected_context) + (let [expected_context (/.some case expected_case)] + (when (/.when case expected_context) {.#Right actual_case} (by equivalence_of_case = expected_case actual_case) @@ -147,13 +148,13 @@ )))) (the whole - (/.Prism Decimal Integer) - (/.prism (function (_ it) - (let [case (decimal.whole it)] - (if (decimal.= it case) - {.#Right (decimal.integer it)} - {.#Left it}))) - integer.decimal)) + (/.Case Decimal Integer) + (/.case (function (_ it) + (let [case (decimal.whole it)] + (if (decimal.= it case) + {.#Right (decimal.integer it)} + {.#Left it}))) + integer.decimal)) (every (Tree it) (Variant @@ -183,9 +184,9 @@ [expected random.integer other random.natural]) (all _.and - (..lens_specification sign - integer.equivalence bit.equivalence - random.integer random.bit) + (..property'_specification sign + integer.equivalence bit.equivalence + random.integer random.bit) (do [! random.monad] [size (by ! each (natural.% 10) random.natural)] (..view_specification ..list_as_stack @@ -194,10 +195,10 @@ (random.list size random.natural) (random.stack size random.natural))) - (prism_specification ..whole - decimal.equivalence integer.equivalence - (by ! each (decimal.* +1,000,000.0) random.unit_decimal) - (by ! each (integer.% +1,000,000) random.integer)) + (case_specification ..whole + decimal.equivalence integer.equivalence + (by ! each (decimal.* +1,000,000.0) random.unit_decimal) + (by ! each (integer.% +1,000,000) random.integer)) (_.coverage [/.revised] (let [is_exception! (or (integer.= +0 expected)