aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/analyser/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/analyser/case
parenta269ea72337852e8e57bd427773baed111ad6e92 (diff)
- Re-organized analysis.
Diffstat (limited to 'new-luxc/source/luxc/analyser/case')
-rw-r--r--new-luxc/source/luxc/analyser/case/coverage.lux299
1 files changed, 0 insertions, 299 deletions
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<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)))))