aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/analyser/case
diff options
context:
space:
mode:
authorEduardo Julian2017-05-30 21:35:37 -0400
committerEduardo Julian2017-05-30 21:35:37 -0400
commitb73f1c909d19d5492d6d9a7dc707a3b817c73619 (patch)
tree369d957687852bb5ca0024e9175072f5c92bf6d1 /new-luxc/source/luxc/analyser/case
parent56b0ca377a30e30bf832d6dfdb789676f67e7ade (diff)
- Documented the analysis phase.
- Some refactoring. - Removed singleton variants.
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/analyser/case.lux294
-rw-r--r--new-luxc/source/luxc/analyser/case/coverage.lux287
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)))))