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. --- new-luxc/source/luxc/analyser/case/coverage.lux | 299 ------------------------ 1 file changed, 299 deletions(-) delete mode 100644 new-luxc/source/luxc/analyser/case/coverage.lux (limited to 'new-luxc/source/luxc/analyser/case') diff --git a/new-luxc/source/luxc/analyser/case/coverage.lux b/new-luxc/source/luxc/analyser/case/coverage.lux deleted file mode 100644 index 554aea1a8..000000000 --- a/new-luxc/source/luxc/analyser/case/coverage.lux +++ /dev/null @@ -1,299 +0,0 @@ -(;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