aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/lang/analysis/case
diff options
context:
space:
mode:
authorEduardo Julian2017-10-31 23:39:49 -0400
committerEduardo Julian2017-10-31 23:39:49 -0400
commit15121222d570f8fe3c5a326208e4f0bad737e63c (patch)
tree88c93ed1f4965fd0e80677df5553a0d47e521963 /new-luxc/source/luxc/lang/analysis/case
parenta269ea72337852e8e57bd427773baed111ad6e92 (diff)
- Re-organized analysis.
Diffstat (limited to 'new-luxc/source/luxc/lang/analysis/case')
-rw-r--r--new-luxc/source/luxc/lang/analysis/case/coverage.lux299
1 files changed, 299 insertions, 0 deletions
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<Bool>]
+ [number]
+ ["e" error "error/" Monad<Error>]
+ text/format
+ (coll [list "list/" Fold<List>]
+ [dict #+ Dict]))
+ [meta "meta/" Monad<Meta>])
+ (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<Meta>
+ [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<Meta>
+ [=sub (determine sub)]
+ (wrap (#Variant num-tags
+ (|> (dict;new number;Hash<Nat>)
+ (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<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 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<Dict> Eq<Coverage>) = casesSF casesA)
+ redundant-pattern
+
+ ## else
+ (do e;Monad<Error>
+ [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<Error>
+ [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<Error>
+ [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<Error>
+ [#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)))))