From 15121222d570f8fe3c5a326208e4f0bad737e63c Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Tue, 31 Oct 2017 23:39:49 -0400 Subject: - Re-organized analysis. --- .../source/luxc/lang/analysis/case/coverage.lux | 299 +++++++++++++++++++++ 1 file changed, 299 insertions(+) create mode 100644 new-luxc/source/luxc/lang/analysis/case/coverage.lux (limited to 'new-luxc/source/luxc/lang/analysis/case/coverage.lux') diff --git a/new-luxc/source/luxc/lang/analysis/case/coverage.lux b/new-luxc/source/luxc/lang/analysis/case/coverage.lux new file mode 100644 index 000000000..554aea1a8 --- /dev/null +++ b/new-luxc/source/luxc/lang/analysis/case/coverage.lux @@ -0,0 +1,299 @@ +(;module: + lux + (lux (control [monad #+ do] + ["ex" exception #+ exception:] + eq) + (data [bool "bool/" Eq] + [number] + ["e" error "error/" Monad] + text/format + (coll [list "list/" Fold] + [dict #+ Dict])) + [meta "meta/" Monad]) + (luxc ["&" base] + (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 "exhaustive" 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 (Dict Nat Coverage)) + (#Seq Coverage Coverage) + (#Alt Coverage Coverage) + #Exhaustive) + +(def: #export (exhaustive? coverage) + (-> Coverage Bool) + (case coverage + (#Exhaustive _) + true + + _ + false)) + +(exception: #export Unknown-Pattern) + +(def: #export (determine pattern) + (-> la;Pattern (Meta Coverage)) + (case pattern + ## Binding amounts to exhaustive coverage because any value can be + ## matched that way. + ## Unit [] amounts to exhaustive coverage because there is only one + ## possible value, so matching against it covers all cases. + (^or (^code ("lux case bind" (~ _))) (^code ("lux case tuple" []))) + (meta/wrap #Exhaustive) + + (^code ("lux case tuple" [(~ singleton)])) + (determine singleton) + + ## Primitive patterns always have partial coverage because there + ## are too many possibilities as far as values go. + (^or [_ (#;Nat _)] [_ (#;Int _)] [_ (#;Deg _)] + [_ (#;Frac _)] [_ (#;Text _)]) + (meta/wrap #Partial) + + ## Bools are the exception, since there is only "true" and + ## "false", which means it is possible for boolean + ## pattern-matching to become exhaustive if complementary parts meet. + [_ (#;Bool value)] + (meta/wrap (#Bool value)) + + ## Tuple patterns can be exhaustive if there is exhaustiveness for all of + ## their sub-patterns. + (^code ("lux case tuple" [(~@ subs)])) + (loop [subs subs] + (case subs + #;Nil + (meta/wrap #Exhaustive) + + (#;Cons sub subs') + (do meta;Monad + [pre (determine sub) + post (recur subs')] + (if (exhaustive? post) + (wrap pre) + (wrap (#Seq pre post)))))) + + ## Variant patterns can be shown to be exhaustive if all the possible + ## cases are handled exhaustively. + (^code ("lux case variant" (~ [_ (#;Nat tag-id)]) (~ [_ (#;Nat num-tags)]) (~ sub))) + (do meta;Monad + [=sub (determine sub)] + (wrap (#Variant num-tags + (|> (dict;new number;Hash) + (dict;put tag-id =sub))))) + + _ + (&;throw Unknown-Pattern (%code pattern)))) + +(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 +## exhaustive, 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 + (e;Error Coverage) + (e;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] + [#Exhaustive #Exhaustive] + true + + [(#Bool sideR) (#Bool sideS)] + (bool/= sideR sideS) + + [(#Variant allR casesR) (#Variant allS casesS)] + (and (n.= allR allS) + (:: (dict;Eq =) = 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 "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 exhaustive and whether it contains +## redundant patterns. +(def: #export (merge addition so-far) + (-> Coverage Coverage (e;Error Coverage)) + (case [addition so-far] + ## The addition cannot possibly improve the coverage. + [_ #Exhaustive] + redundant-pattern + + ## The addition completes the coverage. + [#Exhaustive _] + (error/wrap #Exhaustive) + + [#Partial #Partial] + (error/wrap #Partial) + + ## 2 boolean coverages are exhaustive if they compliment one another. + (^multi [(#Bool sideA) (#Bool sideSF)] + (xor sideA sideSF)) + (error/wrap #Exhaustive) + + [(#Variant allA casesA) (#Variant allSF casesSF)] + (cond (not (n.= allSF allA)) + (e;fail "Variants do not match.") + + (:: (dict;Eq Eq) = casesSF casesA) + redundant-pattern + + ## else + (do e;Monad + [casesM (monad;fold @ + (function [[tagA coverageA] casesSF'] + (case (dict;get tagA casesSF') + (#;Some coverageSF) + (do @ + [coverageM (merge coverageA coverageSF)] + (wrap (dict;put tagA coverageM casesSF'))) + + #;None + (wrap (dict;put tagA coverageA casesSF')))) + casesSF (dict;entries casesA))] + (wrap (if (let [case-coverages (dict;values casesM)] + (and (n.= allSF (list;size case-coverages)) + (list;every? exhaustive? case-coverages))) + #Exhaustive + (#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] + (error/wrap (#Alt so-far addition)) + + ## Same prefix + [true false] + (do e;Monad + [rightM (merge rightA rightSF)] + (if (exhaustive? rightM) + ## If all that follows is exhaustive, then it can be safely dropped + ## (since only the "left" part would influence whether the + ## merged coverage is exhaustive or not). + (wrap leftSF) + (wrap (#Seq leftSF rightM)))) + + ## Same suffix + [false true] + (do e;Monad + [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)) + (error/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 e;Monad + [#let [fuse-once (: (-> Coverage (List Coverage) + (e;Error [(Maybe Coverage) + (List Coverage)])) + (function [coverage possibilities] + (loop [alts possibilities] + (case alts + #;Nil + (wrap [#;None (list coverage)]) + + (#;Cons alt alts') + (case (merge coverage alt) + (#e;Success altM) + (case altM + (#Alt _) + (do @ + [[success alts+] (recur alts')] + (wrap [success (#;Cons alt alts+)])) + + _ + (wrap [(#;Some altM) alts'])) + + (#e;Error error) + (e;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) + (#;Cons last prevs) + (wrap (list/fold (function [left right] (#Alt left right)) + last + prevs)) + + #;Nil + (undefined))))) + + _ + (if (C/= so-far addition) + ## The addition cannot possibly improve the coverage. + redundant-pattern + ## There are now 2 alternative paths. + (error/wrap (#Alt so-far addition))))) -- cgit v1.2.3