diff options
Diffstat (limited to '')
| -rw-r--r-- | new-luxc/source/luxc/analyser/case.lux | 294 | ||||
| -rw-r--r-- | new-luxc/source/luxc/analyser/case/coverage.lux | 287 |
2 files changed, 325 insertions, 256 deletions
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux index f3eec6b6b..306618caf 100644 --- a/new-luxc/source/luxc/analyser/case.lux +++ b/new-luxc/source/luxc/analyser/case.lux @@ -15,25 +15,25 @@ (macro [code]) [type] (type ["TC" check])) - (luxc ["&" base] - (lang ["la" analysis]) - ["&;" env] - (analyser ["&;" common] - ["&;" structure]))) - -(type: #rec Coverage - #PartialC - (#BoolC Bool) - (#VariantC Nat (D;Dict Nat Coverage)) - (#SeqC Coverage Coverage) - (#AltC Coverage Coverage) - #TotalC) + (../.. ["&" base] + (lang ["la" analysis]) + ["&;" env]) + (.. ["&;" common] + ["&;" structure]) + (. ["&&;" coverage])) (def: (pattern-error type pattern) (-> Type Code Text) (format "Cannot match this type: " (%type type) "\n" " With this pattern: " (%code pattern))) +## Type-checking on the input value is done during the analysis of a +## "case" expression, to ensure that the patterns being used make +## sense for the type of the input value. +## Sometimes, that input value is complex, by depending on +## type-variables or quantifications. +## This function makes it easier for "case" analysis to properly +## type-check the input with respect to the patterns. (def: (simplify-case-type type) (-> Type (Lux Type)) (case type @@ -60,6 +60,22 @@ _ (:: Monad<Lux> wrap type))) +## This function handles several concerns at once, but it must be that +## way because those concerns are interleaved when doing +## pattern-matching and they cannot be separated. +## The pattern is analysed in order to get a general feel for what is +## expected of the input value. This, in turn, informs the +## type-checking of the input. +## A kind of "continuation" value is passed around which signifies +## what needs to be done _after_ analysing a pattern. +## In general, this is done to analyse the "body" expression +## associated to a particular pattern _in the context of_ said +## pattern. +## The reason why *context* is important is because patterns may bind +## values to local variables, which may in turn be referenced in the +## body expressions. +## That is why the body must be analysed in the context of the +## pattern, and not separately. (def: (analyse-pattern num-tags inputT pattern next) (All [a] (-> (Maybe Nat) Type Code (Lux a) (Lux [la;Pattern a]))) (case pattern @@ -143,10 +159,10 @@ (&;fail (pattern-error inputT pattern)) ))) - [cursor (#;Record pairs)] + [cursor (#;Record record)] (do Monad<Lux> - [pairs (&structure;normalize-record pairs) - [members recordT] (&structure;order-record pairs) + [record (&structure;normalize record) + [members recordT] (&structure;order record) _ (&;within-type-env (TC;check inputT recordT))] (analyse-pattern (#;Some (list;size members)) inputT [cursor (#;Tuple members)] next)) @@ -200,240 +216,6 @@ (&;fail (format "Unrecognized pattern syntax: " (%code pattern))) )) -(def: (analyse-branch analyse inputT pattern body) - (-> &;Analyser Type Code Code (Lux [la;Pattern la;Analysis])) - (analyse-pattern #;None inputT pattern (analyse body))) - -(do-template [<name> <tag>] - [(def: (<name> coverage) - (-> Coverage Bool) - (case coverage - (<tag> _) - true - - _ - false))] - - [total? #TotalC] - [alt? #AltC] - ) - -(def: (determine-coverage pattern) - (-> la;Pattern Coverage) - (case pattern - (^or (#la;BindP _) (^ (#la;TupleP (list)))) - #TotalC - - (^ (#la;TupleP (list singleton))) - (determine-coverage singleton) - - (#la;BoolP value) - (#BoolC value) - - (^or (#la;NatP _) (#la;IntP _) (#la;DegP _) - (#la;RealP _) (#la;CharP _) (#la;TextP _)) - #PartialC - - (#la;TupleP subs) - (loop [subs subs] - (case subs - #;Nil - #TotalC - - (#;Cons sub subs') - (let [post (recur subs')] - (if (total? post) - (determine-coverage sub) - (#SeqC (determine-coverage sub) - post))))) - - (#la;VariantP tag-id num-tags sub) - (#VariantC num-tags - (|> (D;new number;Hash<Nat>) - (D;put tag-id (determine-coverage sub)))))) - -(def: (xor left right) - (-> Bool Bool Bool) - (or (and left (not right)) - (and (not left) right))) - -(def: redundant-pattern - (R;Result Coverage) - (R;fail "Redundant pattern.")) - -(def: (flatten-alt coverage) - (-> Coverage (List Coverage)) - (case coverage - (#AltC left right) - (list& left (flatten-alt right)) - - _ - (list coverage))) - -(struct: _ (Eq Coverage) - (def: (= reference sample) - (case [reference sample] - [#TotalC #TotalC] - true - - [(#BoolC sideR) (#BoolC sideS)] - (B/= sideR sideS) - - [(#VariantC allR casesR) (#VariantC allS casesS)] - (and (n.= allR allS) - (:: (D;Eq<Dict> =) = casesR casesS)) - - [(#SeqC leftR rightR) (#SeqC leftS rightS)] - (and (= leftR leftS) - (= rightR rightS)) - - [(#AltC _) (#AltC _)] - (let [flatR (flatten-alt reference) - flatS (flatten-alt sample)] - (and (n.= (list;size flatR) (list;size flatS)) - (list;every? (function [[coverageR coverageS]] - (= coverageR coverageS)) - (list;zip2 flatR flatS)))) - - _ - false))) - -(open Eq<Coverage> "C/") - -(def: (merge-coverages addition so-far) - (-> Coverage Coverage (R;Result Coverage)) - (case [addition so-far] - ## The addition cannot possibly improve the coverage. - [_ #TotalC] - redundant-pattern - - ## The addition completes the coverage. - [#TotalC _] - (R/wrap #TotalC) - - [#PartialC #PartialC] - (R/wrap #PartialC) - - (^multi [(#BoolC sideA) (#BoolC sideSF)] - (xor sideA sideSF)) - (R/wrap #TotalC) - - [(#VariantC allA casesA) (#VariantC allSF casesSF)] - (cond (not (n.= allSF allA)) - (R;fail "Variants do not match.") - - (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA) - redundant-pattern - - ## else - (do R;Monad<Result> - [casesM (foldM @ - (function [[tagA coverageA] casesSF'] - (case (D;get tagA casesSF') - (#;Some coverageSF) - (do @ - [coverageM (merge-coverages coverageA coverageSF)] - (wrap (D;put tagA coverageM casesSF'))) - - #;None - (wrap (D;put tagA coverageA casesSF')))) - casesSF (D;entries casesA))] - (wrap (if (let [case-coverages (D;values casesM)] - (and (n.= allSF (list;size case-coverages)) - (list;every? total? case-coverages))) - #TotalC - (#VariantC allSF casesM))))) - - [(#SeqC leftA rightA) (#SeqC leftSF rightSF)] - (case [(C/= leftSF leftA) (C/= rightSF rightA)] - ## There is nothing the addition adds to the coverage. - [true true] - redundant-pattern - - ## The 2 sequences cannot possibly be merged. - [false false] - (R/wrap (#AltC so-far addition)) - - ## Same prefix - [true false] - (do R;Monad<Result> - [rightM (merge-coverages rightA rightSF)] - (if (total? rightM) - (wrap leftSF) - (wrap (#SeqC leftSF rightM)))) - - ## Same suffix - [false true] - (do R;Monad<Result> - [leftM (merge-coverages leftA leftSF)] - (wrap (#SeqC leftM rightA)))) - - ## The left part will always match, so the addition is redundant. - (^multi [(#SeqC left right) single] - (C/= left single)) - redundant-pattern - - ## The right part is not necessary, since it can always match the left. - (^multi [single (#SeqC left right)] - (C/= left single)) - (R/wrap single) - - [_ (#AltC leftS rightS)] - (do R;Monad<Result> - [#let [fuse-once (: (-> Coverage (List Coverage) - (R;Result [(Maybe Coverage) - (List Coverage)])) - (function [coverage possibilities] - (loop [alts possibilities] - (case alts - #;Nil - (wrap [#;None (list coverage)]) - - (#;Cons alt alts') - (case (merge-coverages coverage alt) - (#R;Success altM) - (case altM - (#AltC _) - (do @ - [[success alts+] (recur alts')] - (wrap [success (#;Cons alt alts+)])) - - _ - (wrap [(#;Some altM) alts'])) - - (#R;Error error) - (R;fail error)) - ))))] - [success possibilities] (fuse-once addition (flatten-alt so-far))] - (loop [success success - possibilities possibilities] - (case success - (#;Some coverage') - (do @ - [[success' possibilities'] (fuse-once coverage' possibilities)] - (recur success' possibilities')) - - #;None - (case (list;reverse possibilities) - #;Nil - (R;fail "{ This is not supposed to happen... }") - - (#;Cons last prevs) - (wrap (L/fold (function [left right] (#AltC left right)) - last - prevs)))))) - - _ - (if (C/= so-far addition) - ## The addition cannot possibly improve the coverage. - redundant-pattern - ## There are now 2 alternative paths. - (R/wrap (#AltC so-far addition))))) - -(def: get-coverage - (-> [la;Pattern la;Analysis] Coverage) - (|>. product;left determine-coverage)) - (def: #export (analyse-case analyse input branches) (-> &;Analyser Code (List [Code Code]) (Lux la;Analysis)) (case branches @@ -444,17 +226,17 @@ (do Monad<Lux> [[inputT inputA] (&common;with-unknown-type (analyse input)) - outputH (analyse-branch analyse inputT patternH bodyH) + outputH (analyse-pattern #;None inputT patternH (analyse bodyH)) outputT (mapM @ (function [[patternT bodyT]] - (analyse-branch analyse inputT patternT bodyT)) + (analyse-pattern #;None inputT patternT (analyse bodyT))) branchesT) _ (case (foldM R;Monad<Result> - merge-coverages - (get-coverage outputH) - (L/map get-coverage outputT)) + &&coverage;merge + (|> outputH product;left &&coverage;determine) + (L/map (|>. product;left &&coverage;determine) outputT)) (#R;Success coverage) - (if (total? coverage) + (if (&&coverage;total? coverage) (wrap []) (&;fail "Pattern-matching is not total.")) diff --git a/new-luxc/source/luxc/analyser/case/coverage.lux b/new-luxc/source/luxc/analyser/case/coverage.lux new file mode 100644 index 000000000..754e555b2 --- /dev/null +++ b/new-luxc/source/luxc/analyser/case/coverage.lux @@ -0,0 +1,287 @@ +(;module: + lux + (lux (control monad + eq) + (data [bool "B/" Eq<Bool>] + [number] + ["R" result "R/" Monad<Result>] + (coll [list "L/" Fold<List>] + ["D" dict]))) + (luxc (lang ["la" analysis]))) + +## The coverage of a pattern-matching expression summarizes how well +## all the possible values of an input are being covered by the +## different patterns involved. +## Ideally, the pattern-matching has "total" coverage, which just +## means that every possible value can be matched by at least 1 +## pattern. +## Every other coverage is considered partial, and it would be valued +## as insuficient (since it could lead to runtime errors due to values +## not being handled by any pattern). +## The #Partial tag covers arbitrary partial coverages in a general +## way, while the other tags cover more specific cases for booleans +## and variants. +(type: #export #rec Coverage + #Partial + (#Bool Bool) + (#Variant Nat (D;Dict Nat Coverage)) + (#Seq Coverage Coverage) + (#Alt Coverage Coverage) + #Total) + +(def: #export (total? coverage) + (-> Coverage Bool) + (case coverage + (#Total _) + true + + _ + false)) + +(def: #export (determine pattern) + (-> la;Pattern Coverage) + (case pattern + ## Binding amounts to total coverage because any value can be + ## matched that way. + ## Unit [] amounts to total coverage because there is only one + ## possible value, so matching against it covers all cases. + (^or (#la;BindP _) (^ (#la;TupleP (list)))) + #Total + + (^ (#la;TupleP (list singleton))) + (determine singleton) + + ## Primitive patterns always have partial coverage because there + ## are too many possibilities as far as values go. + (^or (#la;NatP _) (#la;IntP _) (#la;DegP _) + (#la;RealP _) (#la;CharP _) (#la;TextP _)) + #Partial + + ## Bools are the exception, since there is only "true" and + ## "false", which means it is possible for boolean + ## pattern-matching to become total if complementary parts meet. + (#la;BoolP value) + (#Bool value) + + ## Tuple patterns can be total if there is totality for all of + ## their sub-patterns. + (#la;TupleP subs) + (loop [subs subs] + (case subs + #;Nil + #Total + + (#;Cons sub subs') + (let [post (recur subs')] + (if (total? post) + (determine sub) + (#Seq (determine sub) + post))))) + + ## Variant patterns can be shown to be total if all the possible + ## cases are handled totally. + (#la;VariantP tag-id num-tags sub) + (#Variant num-tags + (|> (D;new number;Hash<Nat>) + (D;put tag-id (determine sub)))))) + +(def: (xor left right) + (-> Bool Bool Bool) + (or (and left (not right)) + (and (not left) right))) + +## The coverage checker not only verifies that pattern-matching is +## total, but also that there are no redundant patterns. +## Redundant patterns will never be executed, since there will +## always be a pattern prior to them that would match the input. +## Because of that, the presence of redundant patterns is assumed to +## be a bug, likely due to programmer carelessness. +(def: redundant-pattern + (R;Result Coverage) + (R;fail "Redundant pattern.")) + +(def: (flatten-alt coverage) + (-> Coverage (List Coverage)) + (case coverage + (#Alt left right) + (list& left (flatten-alt right)) + + _ + (list coverage))) + +(struct: _ (Eq Coverage) + (def: (= reference sample) + (case [reference sample] + [#Total #Total] + true + + [(#Bool sideR) (#Bool sideS)] + (B/= sideR sideS) + + [(#Variant allR casesR) (#Variant allS casesS)] + (and (n.= allR allS) + (:: (D;Eq<Dict> =) = casesR casesS)) + + [(#Seq leftR rightR) (#Seq leftS rightS)] + (and (= leftR leftS) + (= rightR rightS)) + + [(#Alt _) (#Alt _)] + (let [flatR (flatten-alt reference) + flatS (flatten-alt sample)] + (and (n.= (list;size flatR) (list;size flatS)) + (list;every? (function [[coverageR coverageS]] + (= coverageR coverageS)) + (list;zip2 flatR flatS)))) + + _ + false))) + +(open Eq<Coverage> "C/") + +## After determining the coverage of each individual pattern, it is +## necessary to merge them all to figure out if the entire +## pattern-matching expression is total and whether it contains +## redundant patterns. +(def: #export (merge addition so-far) + (-> Coverage Coverage (R;Result Coverage)) + (case [addition so-far] + ## The addition cannot possibly improve the coverage. + [_ #Total] + redundant-pattern + + ## The addition completes the coverage. + [#Total _] + (R/wrap #Total) + + [#Partial #Partial] + (R/wrap #Partial) + + ## 2 boolean coverages are total if they compliment one another. + (^multi [(#Bool sideA) (#Bool sideSF)] + (xor sideA sideSF)) + (R/wrap #Total) + + [(#Variant allA casesA) (#Variant allSF casesSF)] + (cond (not (n.= allSF allA)) + (R;fail "Variants do not match.") + + (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA) + redundant-pattern + + ## else + (do R;Monad<Result> + [casesM (foldM @ + (function [[tagA coverageA] casesSF'] + (case (D;get tagA casesSF') + (#;Some coverageSF) + (do @ + [coverageM (merge coverageA coverageSF)] + (wrap (D;put tagA coverageM casesSF'))) + + #;None + (wrap (D;put tagA coverageA casesSF')))) + casesSF (D;entries casesA))] + (wrap (if (let [case-coverages (D;values casesM)] + (and (n.= allSF (list;size case-coverages)) + (list;every? total? case-coverages))) + #Total + (#Variant allSF casesM))))) + + [(#Seq leftA rightA) (#Seq leftSF rightSF)] + (case [(C/= leftSF leftA) (C/= rightSF rightA)] + ## There is nothing the addition adds to the coverage. + [true true] + redundant-pattern + + ## The 2 sequences cannot possibly be merged. + [false false] + (R/wrap (#Alt so-far addition)) + + ## Same prefix + [true false] + (do R;Monad<Result> + [rightM (merge rightA rightSF)] + (if (total? rightM) + ## If all that follows is total, then it can be safely dropped + ## (since only the "left" part would influence whether the + ## merged coverage is total or not). + (wrap leftSF) + (wrap (#Seq leftSF rightM)))) + + ## Same suffix + [false true] + (do R;Monad<Result> + [leftM (merge leftA leftSF)] + (wrap (#Seq leftM rightA)))) + + ## The left part will always match, so the addition is redundant. + (^multi [(#Seq left right) single] + (C/= left single)) + redundant-pattern + + ## The right part is not necessary, since it can always match the left. + (^multi [single (#Seq left right)] + (C/= left single)) + (R/wrap single) + + ## When merging a new coverage against one based on Alt, it may be + ## that one of the many coverages in the Alt is complementary to + ## the new one, so effort must be made to fuse carefully, to match + ## the right coverages together. + ## If one of the Alt sub-coverages matches the new one, the cycle + ## must be repeated, in case the resulting coverage can now match + ## other ones in the original Alt. + ## This process must be repeated until no further productive + ## merges can be done. + [_ (#Alt leftS rightS)] + (do R;Monad<Result> + [#let [fuse-once (: (-> Coverage (List Coverage) + (R;Result [(Maybe Coverage) + (List Coverage)])) + (function [coverage possibilities] + (loop [alts possibilities] + (case alts + #;Nil + (wrap [#;None (list coverage)]) + + (#;Cons alt alts') + (case (merge coverage alt) + (#R;Success altM) + (case altM + (#Alt _) + (do @ + [[success alts+] (recur alts')] + (wrap [success (#;Cons alt alts+)])) + + _ + (wrap [(#;Some altM) alts'])) + + (#R;Error error) + (R;fail error)) + ))))] + [success possibilities] (fuse-once addition (flatten-alt so-far))] + (loop [success success + possibilities possibilities] + (case success + (#;Some coverage') + (do @ + [[success' possibilities'] (fuse-once coverage' possibilities)] + (recur success' possibilities')) + + #;None + (case (list;reverse possibilities) + #;Nil + (R;fail "{ This is not supposed to happen... }") + + (#;Cons last prevs) + (wrap (L/fold (function [left right] (#Alt left right)) + last + prevs)))))) + + _ + (if (C/= so-far addition) + ## The addition cannot possibly improve the coverage. + redundant-pattern + ## There are now 2 alternative paths. + (R/wrap (#Alt so-far addition))))) |