From ddc39860cc86e849d7c9d2d023a7d71f499ff859 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 2 May 2024 01:57:12 -0400 Subject: [PATCH] Added member (a.k.a. Traversal) (part 3 of optics). --- stdlib/source/library/lux/optic.lux | 95 +++++++++++++++++++++++- stdlib/source/library/lux/type/check.lux | 68 +++++++++-------- stdlib/source/test/lux/optic.lux | 21 ++++++ 3 files changed, 151 insertions(+), 33 deletions(-) diff --git a/stdlib/source/library/lux/optic.lux b/stdlib/source/library/lux/optic.lux index 056847640..20ce5c18c 100644 --- a/stdlib/source/library/lux/optic.lux +++ b/stdlib/source/library/lux/optic.lux @@ -6,7 +6,13 @@ [lux (.except macro its revised has as - when)]]) + when + all with) + [abstract + [functor (.only Functor)]] + [type + ["[0]" nominal]] + ["[0]" function]]]) (the macro (<| (.in_module# .prelude) @@ -130,3 +136,90 @@ [when When #when] [some Some #some] ) + +... TODO: Make this nominal type unnecessary. +(nominal.every .public (Membership one all) + (Variant + {#All all} + {#One one (Membership one (-> one all))}) + + (the outer + (for_any (_ one all) + (-> (Membership one all) + (Or all (And one (Membership one (-> one all)))))) + (|>> nominal.reification)) + + (the inner + (for_any (_ one all) + (-> (Or all (And one (Membership one (-> one all)))) + (Membership one all))) + (|>> nominal.abstraction)) + + (the .public membership_functor + (for_any (_ one) + (Functor (Membership one))) + (implementation + (the (each value it) + (nominal.abstraction + (.when (nominal.reification it) + {#All all} + {#All (value all)} + + {#One one next} + {#One one (each (function (_ before) + (|>> before + value)) + next)})) + ))) + + (every .public (Apply context) + (Interface + (is (Functor context) + functor) + (is (for_any (_ it) + (-> it + (context it))) + pure) + (is (for_any (_ it it') + (-> (context (-> it it')) + (-> (context it) + (context it')))) + with))) + + (the .public membership_apply + (for_any (_ one) + (Apply (Membership one))) + (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} + (nominal.abstraction + {#One one (with (by ..membership_functor each function.flipped effect) + cause)}))))) + + (the .public (one it) + (for_any (_ it) + (-> it + (Membership it it))) + (nominal.abstraction {#One it (nominal.abstraction {#All (|>>)})})) + + (the .public (all it) + (for_any (_ one all) + (-> (Membership one all) + all)) + (.when (nominal.reification it) + {#All it} + it + + {#One one next} + ((all next) one)) + )) + +(every .public (Member all one) + (-> all + (Membership one all))) diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux index 9a64cc0a3..10f242477 100644 --- a/stdlib/source/library/lux/type/check.lux +++ b/stdlib/source/library/lux/type/check.lux @@ -9,11 +9,13 @@ [functor (.only Functor)] [monad (.only Monad do)]] [control - ["[0]" maybe]] + ["[0]" maybe] + ["[0]" state]] [error ["[0]" try (.only Try) (.use "[1]#[0]" functor)] ["[0]" exception (.only Exception)]] [function + [predicate (.only Predicate)] ["[0]" mixin (.only Mixin)]] [data ["[0]" product] @@ -24,7 +26,8 @@ ["[0]" set (.only Set)]]] [math [number - ["n" natural (.use "[1]#[0]" base_10)]]] + ["n" natural (.use "[1]#[0]" base_10)] + ["[0]" i64]]] [macro ["^" pattern] ["[0]" template]]]] @@ -48,39 +51,16 @@ (list ["Super type" (//.absolute_text super)] ["Sub type" (//.absolute_text sub)]))) -(every .public (Check it) - (-> Type_Context - (Try [Type_Context it]))) - -(the .public functor - (Functor Check) - (implementation - (the (each f fa) - (function (_ context) - (when (fa context) - {try.#Success [context' output]} - {try.#Success [context' (f output)]} - - {try.#Failure error} - {try.#Failure error}))))) +(every .public Check + (state.With Type_Context Try)) (the .public monad (Monad Check) - (implementation - (the functor ..functor) - - (the (in x) - (function (_ context) - {try.#Success [context x]})) + (state.with try.monad)) - (the (conjoint ffa) - (function (_ context) - (when (ffa context) - {try.#Success [context' fa]} - (fa context') - - {try.#Failure error} - {try.#Failure error}))))) +(the .public functor + (Functor Check) + (by ..monad functor)) (use "/#[0]" ..monad) @@ -617,6 +597,25 @@ (.type (-> [(List Hypothesis) Type Type] (Check (List Hypothesis))))) +(the limit (i64.left_shifted 7 1)) + +(the not_too_many? + (Predicate (List Hypothesis)) + (|>> list.size + (n.< ..limit))) + +(the (hypothesis_as_text it) + (text.Injection Hypothesis) + (text (//.as_text (its #super it)) + " = " + (//.as_text (its #sub it)))) + +(exception.the .public (too_many_hypotheses [it]) + (Exception [(List Hypothesis)]) + (exception.report + (list ["Limit" (n#as limit)] + ["Hypotheses" (exception.listing ..hypothesis_as_text it)]))) + (the (super_reification complete hypotheses super_parameter super_abstraction sub) (-> Complete_Subsumption (List Hypothesis) Type Type Type @@ -625,9 +624,14 @@ #sub sub]] (if (hypothesized? new_hypothesis hypotheses) (/#in hypotheses) + + (not_too_many? hypotheses) (do ..monad [super' (..on (list super_parameter) super_abstraction)] - (complete [(list#composite (list new_hypothesis) hypotheses) super' sub]))))) + (complete [(list#composite (list new_hypothesis) hypotheses) super' sub])) + + ... else + (..except ..too_many_hypotheses [hypotheses])))) (the (opaque_reification complete hypotheses [super_quantification super_parameters] diff --git a/stdlib/source/test/lux/optic.lux b/stdlib/source/test/lux/optic.lux index a44e37973..184de8320 100644 --- a/stdlib/source/test/lux/optic.lux +++ b/stdlib/source/test/lux/optic.lux @@ -153,6 +153,27 @@ {.#Left it}))) integer.decimal)) +(every (Tree it) + (Variant + {#Leaf} + {#Branch (Tree it) it (Tree it)})) + +(the (in_order it) + (for_any (_ it) + (/.Member (Tree it) it)) + (<| (with /.membership_apply) + (when it + {#Leaf} + (pure {#Leaf}) + + {#Branch left it right} + (left_associative with + (pure (function (_ left it right) + {#Branch left it right})) + (in_order left) + (/.one it) + (in_order right))))) + (the .public test Test (<| (_.covering /._)