From 19d38211c33faf6d5fe01665982d696643f60051 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sun, 20 May 2018 20:12:22 -0400 Subject: - Migrated pattern-matching analysis to stdlib. --- new-luxc/source/luxc/lang/analysis/case.lux | 312 -------------------- .../source/luxc/lang/analysis/case/coverage.lux | 300 ------------------- new-luxc/test/test/luxc/lang/analysis/case.lux | 196 ------------- new-luxc/test/test/luxc/lang/analysis/common.lux | 31 -- stdlib/source/lux/lang/analysis.lux | 89 +++--- stdlib/source/lux/lang/analysis/case.lux | 295 +++++++++++++++++++ stdlib/source/lux/lang/analysis/case/coverage.lux | 322 +++++++++++++++++++++ stdlib/source/lux/lang/analysis/structure.lux | 8 +- stdlib/test/test/lux/lang/analysis/case.lux | 194 +++++++++++++ stdlib/test/test/lux/lang/analysis/primitive.lux | 2 +- stdlib/test/test/lux/lang/analysis/structure.lux | 8 +- 11 files changed, 866 insertions(+), 891 deletions(-) delete mode 100644 new-luxc/source/luxc/lang/analysis/case.lux delete mode 100644 new-luxc/source/luxc/lang/analysis/case/coverage.lux delete mode 100644 new-luxc/test/test/luxc/lang/analysis/case.lux delete mode 100644 new-luxc/test/test/luxc/lang/analysis/common.lux create mode 100644 stdlib/source/lux/lang/analysis/case.lux create mode 100644 stdlib/source/lux/lang/analysis/case/coverage.lux create mode 100644 stdlib/test/test/lux/lang/analysis/case.lux diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux deleted file mode 100644 index d9efa2bf4..000000000 --- a/new-luxc/source/luxc/lang/analysis/case.lux +++ /dev/null @@ -1,312 +0,0 @@ -(.module: - lux - (lux (control [monad #+ do] - ["ex" exception #+ exception:] - eq) - (data [bool] - [number] - [product] - ["e" error] - [maybe] - [text] - text/format - (coll [list "list/" Fold Monoid Functor])) - [macro] - (macro [code]) - (lang [type] - (type ["tc" check]))) - (luxc ["&" lang] - (lang ["&." scope] - ["la" analysis] - (analysis [".A" common] - [".A" structure] - (case [".A" coverage]))))) - -(do-template [] - [(exception: #export ( {message Text}) - message)] - - [Cannot-Match-Type-With-Pattern] - [Sum-Type-Has-No-Case] - [Unrecognized-Pattern-Syntax] - [Cannot-Simplify-Type-For-Pattern-Matching] - [Cannot-Have-Empty-Branches] - [Non-Exhaustive-Pattern-Matching] - [Symbols-Must-Be-Unqualified-Inside-Patterns] - ) - -(def: (pattern-error type pattern) - (-> Type Code Text) - (format " Type: " (%type type) "\n" - "Pattern: " (%code pattern))) - -(def: (re-quantify envs baseT) - (-> (List (List Type)) Type Type) - (case envs - #.Nil - baseT - - (#.Cons head tail) - (re-quantify tail (#.UnivQ head baseT)))) - -## 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 caseT) - (-> Type (Meta Type)) - (loop [envs (: (List (List Type)) - (list)) - caseT caseT] - (case caseT - (#.Var id) - (do macro.Monad - [?caseT' (&.with-type-env - (tc.read id))] - (case ?caseT' - (#.Some caseT') - (recur envs caseT') - - _ - (&.throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))) - - (#.Named name unnamedT) - (recur envs unnamedT) - - (#.UnivQ env unquantifiedT) - (recur (#.Cons env envs) unquantifiedT) - - ## (^template [ ] - ## ( _) - ## (do macro.Monad - ## [[_ instanceT] (&.with-type-env - ## )] - ## (recur (maybe.assume (type.apply (list instanceT) caseT))))) - ## ([#.UnivQ tc.var] - ## [#.ExQ tc.existential]) - - (#.ExQ _) - (do macro.Monad - [[ex-id exT] (&.with-type-env - tc.existential)] - (recur envs (maybe.assume (type.apply (list exT) caseT)))) - - (#.Apply inputT funcT) - (case funcT - (#.Var funcT-id) - (do macro.Monad - [funcT' (&.with-type-env - (do tc.Monad - [?funct' (tc.read funcT-id)] - (case ?funct' - (#.Some funct') - (wrap funct') - - _ - (tc.throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))))] - (recur envs (#.Apply inputT funcT'))) - - _ - (case (type.apply (list inputT) funcT) - (#.Some outputT) - (recur envs outputT) - - #.None - (&.throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))) - - (#.Product _) - (|> caseT - type.flatten-tuple - (list/map (re-quantify envs)) - type.tuple - (:: macro.Monad wrap)) - - _ - (:: macro.Monad wrap (re-quantify envs caseT))))) - -## 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 (Meta a) (Meta [la.Pattern a]))) - (case pattern - [cursor (#.Symbol ["" name])] - (&.with-cursor cursor - (do macro.Monad - [outputA (&scope.with-local [name inputT] - next) - idx &scope.next-local] - (wrap [(` ("lux case bind" (~ (code.nat idx)))) outputA]))) - - [cursor (#.Symbol ident)] - (&.with-cursor cursor - (&.throw Symbols-Must-Be-Unqualified-Inside-Patterns (%ident ident))) - - (^template [ ] - [cursor ( test)] - (&.with-cursor cursor - (do macro.Monad - [_ (&.with-type-env - (tc.check inputT )) - outputA next] - (wrap [pattern outputA])))) - ([Bool #.Bool] - [Nat #.Nat] - [Int #.Int] - [Deg #.Deg] - [Frac #.Frac] - [Text #.Text]) - - (^ [cursor (#.Tuple (list))]) - (&.with-cursor cursor - (do macro.Monad - [_ (&.with-type-env - (tc.check inputT Top)) - outputA next] - (wrap [(` ("lux case tuple" [])) outputA]))) - - (^ [cursor (#.Tuple (list singleton))]) - (analyse-pattern #.None inputT singleton next) - - [cursor (#.Tuple sub-patterns)] - (&.with-cursor cursor - (do macro.Monad - [inputT' (simplify-case-type inputT)] - (case inputT' - (#.Product _) - (let [sub-types (type.flatten-tuple inputT') - num-sub-types (maybe.default (list.size sub-types) - num-tags) - num-sub-patterns (list.size sub-patterns) - matches (cond (n/< num-sub-types num-sub-patterns) - (let [[prefix suffix] (list.split (n/dec num-sub-patterns) sub-types)] - (list.zip2 (list/compose prefix (list (type.tuple suffix))) sub-patterns)) - - (n/> num-sub-types num-sub-patterns) - (let [[prefix suffix] (list.split (n/dec num-sub-types) sub-patterns)] - (list.zip2 sub-types (list/compose prefix (list (code.tuple suffix))))) - - ## (n/= num-sub-types num-sub-patterns) - (list.zip2 sub-types sub-patterns) - )] - (do @ - [[memberP+ thenA] (list/fold (: (All [a] - (-> [Type Code] (Meta [(List la.Pattern) a]) - (Meta [(List la.Pattern) a]))) - (function (_ [memberT memberC] then) - (do @ - [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Meta a) (Meta [la.Pattern a]))) - analyse-pattern) - #.None memberT memberC then)] - (wrap [(list& memberP memberP+) thenA])))) - (do @ - [nextA next] - (wrap [(list) nextA])) - (list.reverse matches))] - (wrap [(` ("lux case tuple" [(~+ memberP+)])) - thenA]))) - - _ - (&.throw Cannot-Match-Type-With-Pattern (pattern-error inputT pattern)) - ))) - - [cursor (#.Record record)] - (do macro.Monad - [record (structureA.normalize record) - [members recordT] (structureA.order record) - _ (&.with-type-env - (tc.check inputT recordT))] - (analyse-pattern (#.Some (list.size members)) inputT [cursor (#.Tuple members)] next)) - - [cursor (#.Tag tag)] - (&.with-cursor cursor - (analyse-pattern #.None inputT (` ((~ pattern))) next)) - - (^ [cursor (#.Form (list& [_ (#.Nat idx)] values))]) - (&.with-cursor cursor - (do macro.Monad - [inputT' (simplify-case-type inputT)] - (case inputT' - (#.Sum _) - (let [flat-sum (type.flatten-variant inputT') - size-sum (list.size flat-sum) - num-cases (maybe.default size-sum num-tags)] - (case (list.nth idx flat-sum) - (^multi (#.Some case-type) - (n/< num-cases idx)) - (if (and (n/> num-cases size-sum) - (n/= (n/dec num-cases) idx)) - (do macro.Monad - [[testP nextA] (analyse-pattern #.None - (type.variant (list.drop (n/dec num-cases) flat-sum)) - (` [(~+ values)]) - next)] - (wrap [(` ("lux case variant" (~ (code.nat idx)) (~ (code.nat num-cases)) (~ testP))) - nextA])) - (do macro.Monad - [[testP nextA] (analyse-pattern #.None case-type (` [(~+ values)]) next)] - (wrap [(` ("lux case variant" (~ (code.nat idx)) (~ (code.nat num-cases)) (~ testP))) - nextA]))) - - _ - (&.throw Sum-Type-Has-No-Case - (format "Case: " (%n idx) "\n" - "Type: " (%type inputT))))) - - _ - (&.throw Cannot-Match-Type-With-Pattern (pattern-error inputT pattern))))) - - (^ [cursor (#.Form (list& [_ (#.Tag tag)] values))]) - (&.with-cursor cursor - (do macro.Monad - [tag (macro.normalize tag) - [idx group variantT] (macro.resolve-tag tag) - _ (&.with-type-env - (tc.check inputT variantT))] - (analyse-pattern (#.Some (list.size group)) inputT (` ((~ (code.nat idx)) (~+ values))) next))) - - _ - (&.throw Unrecognized-Pattern-Syntax (%code pattern)) - )) - -(def: #export (analyse-case analyse inputC branches) - (-> &.Analyser Code (List [Code Code]) (Meta la.Analysis)) - (case branches - #.Nil - (&.throw Cannot-Have-Empty-Branches "") - - (#.Cons [patternH bodyH] branchesT) - (do macro.Monad - [[inputT inputA] (commonA.with-unknown-type - (analyse inputC)) - outputH (analyse-pattern #.None inputT patternH (analyse bodyH)) - outputT (monad.map @ - (function (_ [patternT bodyT]) - (analyse-pattern #.None inputT patternT (analyse bodyT))) - branchesT) - outputHC (|> outputH product.left coverageA.determine) - outputTC (monad.map @ (|>> product.left coverageA.determine) outputT) - _ (case (monad.fold e.Monad coverageA.merge outputHC outputTC) - (#e.Success coverage) - (&.assert Non-Exhaustive-Pattern-Matching "" - (coverageA.exhaustive? coverage)) - - (#e.Error error) - (&.fail error))] - (wrap (` ("lux case" (~ inputA) (~ (code.record (list& outputH outputT))))))))) diff --git a/new-luxc/source/luxc/lang/analysis/case/coverage.lux b/new-luxc/source/luxc/lang/analysis/case/coverage.lux deleted file mode 100644 index 38f977011..000000000 --- a/new-luxc/source/luxc/lang/analysis/case/coverage.lux +++ /dev/null @@ -1,300 +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] - (dictionary ["dict" unordered #+ Dict]))) - [macro "macro/" Monad]) - (luxc ["&" lang] - (lang ["la" analysis]))) - -(exception: #export (Unknown-Pattern {message Text}) - message) - -## 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)) - -(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" []))) - (macro/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 _)]) - (macro/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)] - (macro/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 - (macro/wrap #Exhaustive) - - (#.Cons sub subs') - (do macro.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 macro.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))))) diff --git a/new-luxc/test/test/luxc/lang/analysis/case.lux b/new-luxc/test/test/luxc/lang/analysis/case.lux deleted file mode 100644 index 63dd60e14..000000000 --- a/new-luxc/test/test/luxc/lang/analysis/case.lux +++ /dev/null @@ -1,196 +0,0 @@ -(.module: - lux - (lux [io] - (control [monad #+ do] - pipe) - (data [bool "B/" Eq] - ["R" error] - [product] - [maybe] - [text "T/" Eq] - text/format - (coll [list "L/" Monad] - (set ["set" unordered]))) - ["r" math/random "r/" Monad] - [macro #+ Monad] - (macro [code]) - (lang [type "type/" Eq] - (type ["tc" check])) - test) - (luxc ["&" lang] - (lang ["@." module] - ["la" analysis] - (analysis [".A" expression] - ["@" case] - ["@." common]))) - (// common) - (test/luxc common)) - -(def: (exhaustive-weaving branchings) - (-> (List (List Code)) (List (List Code))) - (case branchings - #.Nil - #.Nil - - (#.Cons head+ #.Nil) - (L/map (|>> list) head+) - - (#.Cons head+ tail++) - (do list.Monad - [tail+ (exhaustive-weaving tail++) - head head+] - (wrap (#.Cons head tail+))))) - -(def: #export (exhaustive-branches allow-literals? variantTC inputC) - (-> Bool (List [Code Code]) Code (r.Random (List Code))) - (case inputC - [_ (#.Bool _)] - (r/wrap (list (' true) (' false))) - - (^template [ ] - [_ ( _)] - (if allow-literals? - (do r.Monad - [?sample (r.maybe )] - (case ?sample - (#.Some sample) - (do @ - [else (exhaustive-branches allow-literals? variantTC inputC)] - (wrap (list& ( sample) else))) - - #.None - (wrap (list (' _))))) - (r/wrap (list (' _))))) - ([#.Nat r.nat code.nat] - [#.Int r.int code.int] - [#.Deg r.deg code.deg] - [#.Frac r.frac code.frac] - [#.Text (r.text +5) code.text]) - - (^ [_ (#.Tuple (list))]) - (r/wrap (list (' []))) - - (^ [_ (#.Record (list))]) - (r/wrap (list (' {}))) - - [_ (#.Tuple members)] - (do r.Monad - [member-wise-patterns (monad.map @ (exhaustive-branches allow-literals? variantTC) members)] - (wrap (|> member-wise-patterns - exhaustive-weaving - (L/map code.tuple)))) - - [_ (#.Record kvs)] - (do r.Monad - [#let [ks (L/map product.left kvs) - vs (L/map product.right kvs)] - member-wise-patterns (monad.map @ (exhaustive-branches allow-literals? variantTC) vs)] - (wrap (|> member-wise-patterns - exhaustive-weaving - (L/map (|>> (list.zip2 ks) code.record))))) - - (^ [_ (#.Form (list [_ (#.Tag _)] _))]) - (do r.Monad - [bundles (monad.map @ - (function (_ [_tag _code]) - (do @ - [v-branches (exhaustive-branches allow-literals? variantTC _code)] - (wrap (L/map (function (_ pattern) (` ((~ _tag) (~ pattern)))) - v-branches)))) - variantTC)] - (wrap (L/join bundles))) - - _ - (r/wrap (list)) - )) - -(def: #export (input variant-tags record-tags primitivesC) - (-> (List Code) (List Code) (List Code) (r.Random Code)) - (r.rec - (function (_ input) - ($_ r.either - (r/map product.right gen-primitive) - (do r.Monad - [choice (|> r.nat (:: @ map (n/% (list.size variant-tags)))) - #let [choiceT (maybe.assume (list.nth choice variant-tags)) - choiceC (maybe.assume (list.nth choice primitivesC))]] - (wrap (` ((~ choiceT) (~ choiceC))))) - (do r.Monad - [size (|> r.nat (:: @ map (n/% +3))) - elems (r.list size input)] - (wrap (code.tuple elems))) - (r/wrap (code.record (list.zip2 record-tags primitivesC))) - )))) - -(def: (branch body pattern) - (-> Code Code [Code Code]) - [pattern body]) - -(context: "Pattern-matching." - ## #seed +9253409297339902486 - ## #seed +3793366152923578600 - (<| (seed +5004137551292836565) - ## (times +100) - (do @ - [module-name (r.text +5) - variant-name (r.text +5) - record-name (|> (r.text +5) (r.filter (|>> (T/= variant-name) not))) - size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2)))) - variant-tags (|> (r.set text.Hash size (r.text +5)) (:: @ map set.to-list)) - record-tags (|> (r.set text.Hash size (r.text +5)) (:: @ map set.to-list)) - primitivesTC (r.list size gen-primitive) - #let [primitivesT (L/map product.left primitivesTC) - primitivesC (L/map product.right primitivesTC) - code-tag (|>> [module-name] code.tag) - variant-tags+ (L/map code-tag variant-tags) - record-tags+ (L/map code-tag record-tags) - variantTC (list.zip2 variant-tags+ primitivesC)] - inputC (input variant-tags+ record-tags+ primitivesC) - [outputT outputC] gen-primitive - [heterogeneousT heterogeneousC] (|> gen-primitive - (r.filter (|>> product.left (tc.checks? outputT) not))) - exhaustive-patterns (exhaustive-branches true variantTC inputC) - redundant-patterns (exhaustive-branches false variantTC inputC) - redundancy-idx (|> r.nat (:: @ map (n/% (list.size redundant-patterns)))) - heterogeneous-idx (|> r.nat (:: @ map (n/% (list.size exhaustive-patterns)))) - #let [exhaustive-branchesC (L/map (branch outputC) - exhaustive-patterns) - non-exhaustive-branchesC (list.take (n/dec (list.size exhaustive-branchesC)) - exhaustive-branchesC) - redundant-branchesC (<| (L/map (branch outputC)) - list.concat - (list (list.take redundancy-idx redundant-patterns) - (list (maybe.assume (list.nth redundancy-idx redundant-patterns))) - (list.drop redundancy-idx redundant-patterns))) - heterogeneous-branchesC (list.concat (list (list.take heterogeneous-idx exhaustive-branchesC) - (list (let [[_pattern _body] (maybe.assume (list.nth heterogeneous-idx exhaustive-branchesC))] - [_pattern heterogeneousC])) - (list.drop (n/inc heterogeneous-idx) exhaustive-branchesC))) - analyse-pm (|>> (@.analyse-case analyse inputC) - (&.with-type outputT) - &.with-scope - (do Monad - [_ (@module.declare-tags variant-tags false - (#.Named [module-name variant-name] - (type.variant primitivesT))) - _ (@module.declare-tags record-tags false - (#.Named [module-name record-name] - (type.tuple primitivesT)))]) - (@module.with-module +0 module-name))]] - ($_ seq - (test "Will reject empty pattern-matching (no branches)." - (|> (analyse-pm (list)) - check-failure)) - (test "Can analyse exhaustive pattern-matching." - (|> (analyse-pm exhaustive-branchesC) - check-success)) - (test "Will reject non-exhaustive pattern-matching." - (|> (analyse-pm non-exhaustive-branchesC) - check-failure)) - (test "Will reject redundant pattern-matching." - (|> (analyse-pm redundant-branchesC) - check-failure)) - (test "Will reject pattern-matching if the bodies of the branches do not all have the same type." - (|> (analyse-pm heterogeneous-branchesC) - check-failure)) - )))) diff --git a/new-luxc/test/test/luxc/lang/analysis/common.lux b/new-luxc/test/test/luxc/lang/analysis/common.lux deleted file mode 100644 index 7e343cc88..000000000 --- a/new-luxc/test/test/luxc/lang/analysis/common.lux +++ /dev/null @@ -1,31 +0,0 @@ -(.module: - lux - (lux [io] - (control pipe) - ["r" math/random "r/" Monad] - (data ["e" error]) - [macro] - (macro [code])) - (luxc ["&" lang] - (lang (analysis [".A" expression]) - [eval])) - (test/luxc common)) - -(def: #export analyse - &.Analyser - (expressionA.analyser eval.eval)) - -(do-template [ ] - [(def: #export ( analysis) - (All [a] (-> (Meta a) Bool)) - (|> analysis - (macro.run (io.run init-jvm)) - (case> (#e.Success _) - - - (#e.Error error) - )))] - - [check-success true false] - [check-failure false true] - ) diff --git a/stdlib/source/lux/lang/analysis.lux b/stdlib/source/lux/lang/analysis.lux index 223f2fb29..0b48f803d 100644 --- a/stdlib/source/lux/lang/analysis.lux +++ b/stdlib/source/lux/lang/analysis.lux @@ -48,24 +48,15 @@ (#Constant Ident) (#Special (Special Text))) -(type: #export Variant +(type: #export (Variant a) {#lefts Nat #right? Bool - #value Analysis}) + #value a}) -(type: #export Tuple (List Analysis)) +(type: #export (Tuple a) (List a)) (type: #export Application [Analysis (List Analysis)]) -(do-template [ ] - [(def: - (-> Analysis Analysis) - (|>> #Sum #Structure))] - - [left #.Left] - [right #.Right] - ) - (def: (last? size tag) (-> Nat Tag Bool) (n/= (dec size) tag)) @@ -75,35 +66,47 @@ (let [identity (#Function (list) (#Variable (#Local +1)))] (#Apply value identity))) -(def: #export (sum size tag value) - (-> Nat Tag Analysis Analysis) - (if (last? size tag) - (if (n/= +1 tag) - (..right value) - (list/fold (function.const ..left) - (..right value) - (list.n/range +0 (n/- +2 tag)))) - (list/fold (function.const ..left) - (case value - (#Structure (#Sum _)) - (no-op value) - - _ - value) - (list.n/range +0 tag)))) - -(def: #export (product members) - (-> Tuple Analysis) - (case (list.reverse members) - #.Nil - (#Primitive #Unit) - - (#.Cons singleton #.Nil) - singleton - - (#.Cons last prevs) - (list/fold (function (_ left right) (#Structure (#Product left right))) - last prevs))) +(do-template [ ] + [(def: #export ( size tag value) + (-> Nat Tag ) + (let [left (function.const (|>> #.Left #Sum )) + right (|>> #.Right #Sum )] + (if (last? size tag) + (if (n/= +1 tag) + (right value) + (list/fold left + (right value) + (list.n/range +0 (n/- +2 tag)))) + (list/fold left + (case value + ( (#Sum _)) + ( value) + + _ + value) + (list.n/range +0 tag)))))] + + [sum-analysis Analysis #Structure no-op] + [sum-pattern Pattern #Complex id] + ) + +(do-template [ ] + [(def: #export ( members) + (-> (Tuple ) ) + (case (list.reverse members) + #.Nil + ( #Unit) + + (#.Cons singleton #.Nil) + singleton + + (#.Cons last prevs) + (list/fold (function (_ left right) ( (#Product left right))) + last prevs)))] + + [product-analysis Analysis #Primitive #Structure] + [product-pattern Pattern #Simple #Complex] + ) (def: #export (apply [func args]) (-> Application Analysis) @@ -113,7 +116,7 @@ (-> Code (Meta Analysis))) (def: #export (tuple analysis) - (-> Analysis Tuple) + (-> Analysis (Tuple Analysis)) (case analysis (#Structure (#Product left right)) (#.Cons left (tuple right)) @@ -122,7 +125,7 @@ (list analysis))) (def: #export (variant analysis) - (-> Analysis (Maybe Variant)) + (-> Analysis (Maybe (Variant Analysis))) (loop [lefts +0 variantA analysis] (case variantA diff --git a/stdlib/source/lux/lang/analysis/case.lux b/stdlib/source/lux/lang/analysis/case.lux new file mode 100644 index 000000000..3140a9d7e --- /dev/null +++ b/stdlib/source/lux/lang/analysis/case.lux @@ -0,0 +1,295 @@ +(.module: + [lux #- case] + (lux (control [monad #+ do] + ["ex" exception #+ exception:] + [equality #+ Eq]) + (data [bool] + [number] + [product] + ["e" error] + [maybe] + [text] + text/format + (coll [list "list/" Fold Monoid Functor])) + [function] + [macro] + (macro [code]) + [lang] + (lang [type] + (type ["tc" check]) + [".L" scope] + [".L" analysis #+ Pattern Analysis Analyser] + (analysis [".A" type] + [".A" structure] + (case [".A" coverage]))))) + +(exception: #export (cannot-match-type-with-pattern {type Type} {pattern Code}) + (ex.report ["Type" (%type type)] + ["Pattern" (%code pattern)])) + +(exception: #export (sum-type-has-no-case {case Nat} {type Type}) + (ex.report ["Case" (%n case)] + ["Type" (%type type)])) + +(exception: #export (unrecognized-pattern-syntax {pattern Code}) + (%code pattern)) + +(exception: #export (cannot-simplify-type-for-pattern-matching {type Type}) + (%type type)) + +(do-template [] + [(exception: #export ( {message Text}) + message)] + + [cannot-have-empty-branches] + [non-exhaustive-pattern-matching] + ) + +(def: (re-quantify envs baseT) + (-> (List (List Type)) Type Type) + (.case envs + #.Nil + baseT + + (#.Cons head tail) + (re-quantify tail (#.UnivQ head baseT)))) + +## 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 caseT) + (-> Type (Meta Type)) + (loop [envs (: (List (List Type)) + (list)) + caseT caseT] + (.case caseT + (#.Var id) + (do macro.Monad + [?caseT' (typeA.with-env + (tc.read id))] + (.case ?caseT' + (#.Some caseT') + (recur envs caseT') + + _ + (lang.throw cannot-simplify-type-for-pattern-matching caseT))) + + (#.Named name unnamedT) + (recur envs unnamedT) + + (#.UnivQ env unquantifiedT) + (recur (#.Cons env envs) unquantifiedT) + + (#.ExQ _) + (do macro.Monad + [[ex-id exT] (typeA.with-env + tc.existential)] + (recur envs (maybe.assume (type.apply (list exT) caseT)))) + + (#.Apply inputT funcT) + (.case funcT + (#.Var funcT-id) + (do macro.Monad + [funcT' (typeA.with-env + (do tc.Monad + [?funct' (tc.read funcT-id)] + (.case ?funct' + (#.Some funct') + (wrap funct') + + _ + (tc.throw cannot-simplify-type-for-pattern-matching caseT))))] + (recur envs (#.Apply inputT funcT'))) + + _ + (.case (type.apply (list inputT) funcT) + (#.Some outputT) + (recur envs outputT) + + #.None + (lang.throw cannot-simplify-type-for-pattern-matching caseT))) + + (#.Product _) + (|> caseT + type.flatten-tuple + (list/map (re-quantify envs)) + type.tuple + (:: macro.Monad wrap)) + + _ + (:: macro.Monad wrap (re-quantify envs caseT))))) + +(def: (analyse-primitive type inputT cursor output next) + (All [a] (-> Type Type Cursor Pattern (Meta a) (Meta [Pattern a]))) + (lang.with-cursor cursor + (do macro.Monad + [_ (typeA.with-env + (tc.check inputT type)) + outputA next] + (wrap [output outputA])))) + +## 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 (Meta a) (Meta [Pattern a]))) + (.case pattern + [cursor (#.Symbol ["" name])] + (lang.with-cursor cursor + (do macro.Monad + [outputA (scopeL.with-local [name inputT] + next) + idx scopeL.next-local] + (wrap [(#analysisL.Bind idx) outputA]))) + + (^template [ ] + [cursor ] + (analyse-primitive inputT cursor (#analysisL.Simple ) next)) + ([Bool (#.Bool pattern-value) (#analysisL.Bool pattern-value)] + [Nat (#.Nat pattern-value) (#analysisL.Nat pattern-value)] + [Int (#.Int pattern-value) (#analysisL.Int pattern-value)] + [Deg (#.Deg pattern-value) (#analysisL.Deg pattern-value)] + [Frac (#.Frac pattern-value) (#analysisL.Frac pattern-value)] + [Text (#.Text pattern-value) (#analysisL.Text pattern-value)] + [Top (#.Tuple #.Nil) #analysisL.Unit]) + + (^ [cursor (#.Tuple (list singleton))]) + (analyse-pattern #.None inputT singleton next) + + [cursor (#.Tuple sub-patterns)] + (lang.with-cursor cursor + (do macro.Monad + [inputT' (simplify-case-type inputT)] + (.case inputT' + (#.Product _) + (let [sub-types (type.flatten-tuple inputT') + num-sub-types (maybe.default (list.size sub-types) + num-tags) + num-sub-patterns (list.size sub-patterns) + matches (cond (n/< num-sub-types num-sub-patterns) + (let [[prefix suffix] (list.split (dec num-sub-patterns) sub-types)] + (list.zip2 (list/compose prefix (list (type.tuple suffix))) sub-patterns)) + + (n/> num-sub-types num-sub-patterns) + (let [[prefix suffix] (list.split (dec num-sub-types) sub-patterns)] + (list.zip2 sub-types (list/compose prefix (list (code.tuple suffix))))) + + ## (n/= num-sub-types num-sub-patterns) + (list.zip2 sub-types sub-patterns))] + (do @ + [[memberP+ thenA] (list/fold (: (All [a] + (-> [Type Code] (Meta [(List Pattern) a]) + (Meta [(List Pattern) a]))) + (function (_ [memberT memberC] then) + (do @ + [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Meta a) (Meta [Pattern a]))) + analyse-pattern) + #.None memberT memberC then)] + (wrap [(list& memberP memberP+) thenA])))) + (do @ + [nextA next] + (wrap [(list) nextA])) + (list.reverse matches))] + (wrap [(analysisL.product-pattern memberP+) + thenA]))) + + _ + (lang.throw cannot-match-type-with-pattern [inputT pattern]) + ))) + + [cursor (#.Record record)] + (do macro.Monad + [record (structureA.normalize record) + [members recordT] (structureA.order record) + _ (typeA.with-env + (tc.check inputT recordT))] + (analyse-pattern (#.Some (list.size members)) inputT [cursor (#.Tuple members)] next)) + + [cursor (#.Tag tag)] + (lang.with-cursor cursor + (analyse-pattern #.None inputT (` ((~ pattern))) next)) + + (^ [cursor (#.Form (list& [_ (#.Nat idx)] values))]) + (lang.with-cursor cursor + (do macro.Monad + [inputT' (simplify-case-type inputT)] + (.case inputT' + (#.Sum _) + (let [flat-sum (type.flatten-variant inputT') + size-sum (list.size flat-sum) + num-cases (maybe.default size-sum num-tags)] + (.case (list.nth idx flat-sum) + (^multi (#.Some case-type) + (n/< num-cases idx)) + (do macro.Monad + [[testP nextA] (if (and (n/> num-cases size-sum) + (n/= (dec num-cases) idx)) + (analyse-pattern #.None + (type.variant (list.drop (dec num-cases) flat-sum)) + (` [(~+ values)]) + next) + (analyse-pattern #.None case-type (` [(~+ values)]) next))] + (wrap [(analysisL.sum-pattern num-cases idx testP) + nextA])) + + _ + (lang.throw sum-type-has-no-case [idx inputT]))) + + _ + (lang.throw cannot-match-type-with-pattern [inputT pattern])))) + + (^ [cursor (#.Form (list& [_ (#.Tag tag)] values))]) + (lang.with-cursor cursor + (do macro.Monad + [tag (macro.normalize tag) + [idx group variantT] (macro.resolve-tag tag) + _ (typeA.with-env + (tc.check inputT variantT))] + (analyse-pattern (#.Some (list.size group)) inputT (` ((~ (code.nat idx)) (~+ values))) next))) + + _ + (lang.throw unrecognized-pattern-syntax pattern) + )) + +(def: #export (case analyse inputC branches) + (-> Analyser Code (List [Code Code]) (Meta Analysis)) + (.case branches + #.Nil + (lang.throw cannot-have-empty-branches "") + + (#.Cons [patternH bodyH] branchesT) + (do macro.Monad + [[inputT inputA] (typeA.with-inference + (analyse inputC)) + outputH (analyse-pattern #.None inputT patternH (analyse bodyH)) + outputT (monad.map @ + (function (_ [patternT bodyT]) + (analyse-pattern #.None inputT patternT (analyse bodyT))) + branchesT) + outputHC (|> outputH product.left coverageA.determine) + outputTC (monad.map @ (|>> product.left coverageA.determine) outputT) + _ (.case (monad.fold e.Monad coverageA.merge outputHC outputTC) + (#e.Success coverage) + (lang.assert non-exhaustive-pattern-matching "" + (coverageA.exhaustive? coverage)) + + (#e.Error error) + (lang.fail error))] + (wrap (#analysisL.Case inputA [outputH outputT]))))) diff --git a/stdlib/source/lux/lang/analysis/case/coverage.lux b/stdlib/source/lux/lang/analysis/case/coverage.lux new file mode 100644 index 000000000..da256206f --- /dev/null +++ b/stdlib/source/lux/lang/analysis/case/coverage.lux @@ -0,0 +1,322 @@ +(.module: + lux + (lux (control [monad #+ do] + ["ex" exception #+ exception:] + equality) + (data [bool "bool/" Eq] + [number] + ["e" error "error/" Monad] + [maybe] + text/format + (coll [list "list/" Fold] + (dictionary ["dict" unordered #+ Dict]))) + [macro "macro/" Monad] + [lang] + (lang [".L" analysis #+ Pattern Variant]))) + +(def: cases + (-> (Maybe Nat) Nat) + (|>> (maybe.default +0))) + +(def: (variant sum-side) + (-> (Either Pattern Pattern) (Variant Pattern)) + (loop [lefts +0 + variantP sum-side] + (case variantP + (#.Left valueP) + (case valueP + (#analysisL.Complex (#analysisL.Sum value-side)) + (recur (inc lefts) value-side) + + _ + {#analysisL.lefts lefts + #analysisL.right? false + #analysisL.value valueP}) + + (#.Right valueP) + {#analysisL.lefts lefts + #analysisL.right? true + #analysisL.value valueP}))) + +## 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 (Maybe Nat) (Dict Nat Coverage)) + (#Seq Coverage Coverage) + (#Alt Coverage Coverage) + #Exhaustive) + +(def: #export (exhaustive? coverage) + (-> Coverage Bool) + (case coverage + (#Exhaustive _) + true + + _ + false)) + +(def: #export (determine pattern) + (-> Pattern (Meta Coverage)) + (case pattern + (^or (#analysisL.Simple #analysisL.Unit) + (#analysisL.Bind _)) + (macro/wrap #Exhaustive) + + ## Primitive patterns always have partial coverage because there + ## are too many possibilities as far as values go. + (^template [] + (#analysisL.Simple ( _)) + (macro/wrap #Partial)) + ([#analysisL.Nat] + [#analysisL.Int] + [#analysisL.Deg] + [#analysisL.Frac] + [#analysisL.Text]) + + ## 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. + (#analysisL.Simple (#analysisL.Bool value)) + (macro/wrap (#Bool value)) + + ## Tuple patterns can be exhaustive if there is exhaustiveness for all of + ## their sub-patterns. + (#analysisL.Complex (#analysisL.Product [left right])) + (do macro.Monad + [left (determine left) + right (determine right)] + (case right + (#Exhaustive _) + (wrap left) + + _ + (wrap (#Seq left right)))) + + (#analysisL.Complex (#analysisL.Sum sum-side)) + (let [[variant-lefts variant-right? variant-value] (variant sum-side)] + ## Variant patterns can be shown to be exhaustive if all the possible + ## cases are handled exhaustively. + (do macro.Monad + [value-coverage (determine variant-value) + #let [variant-idx (if variant-right? + (inc variant-lefts) + variant-lefts)]] + (wrap (#Variant (if variant-right? + (#.Some variant-idx) + #.None) + (|> (dict.new number.Hash) + (dict.put variant-idx value-coverage)))))))) + +(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/= (cases allR) + (cases 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/= (cases allSF) (cases 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/= (cases 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))))) diff --git a/stdlib/source/lux/lang/analysis/structure.lux b/stdlib/source/lux/lang/analysis/structure.lux index cc185ebe9..8e3611e67 100644 --- a/stdlib/source/lux/lang/analysis/structure.lux +++ b/stdlib/source/lux/lang/analysis/structure.lux @@ -89,7 +89,7 @@ (do @ [valueA (typeA.with-type variant-type (analyse valueC))] - (wrap (analysis.sum type-size tag valueA))) + (wrap (analysis.sum-analysis type-size tag valueA))) #.None (lang.throw inferenceA.variant-tag-out-of-bounds [type-size tag expectedT]))) @@ -219,7 +219,7 @@ _ (typeA.with-env (tc.check expectedT (type.tuple (list/map product.left membersTA))))] - (wrap (analysis.product (list/map product.right membersTA)))))) + (wrap (analysis.product-analysis (list/map product.right membersTA)))))) (^template [ ] ( _) @@ -268,7 +268,7 @@ [#let [case-size (list.size group)] inferenceT (inferenceA.variant idx case-size variantT) [inferredT valueA+] (inferenceA.general analyse inferenceT (list valueC))] - (wrap (analysis.sum case-size idx (|> valueA+ list.head maybe.assume)))) + (wrap (analysis.sum-analysis case-size idx (|> valueA+ list.head maybe.assume)))) _ (..sum analyse idx valueC)))) @@ -352,7 +352,7 @@ (do @ [inferenceT (inferenceA.record recordT) [inferredT membersA] (inferenceA.general analyse inferenceT membersC)] - (wrap (analysis.product membersA))) + (wrap (analysis.product-analysis membersA))) _ (..product analyse membersC)))))) diff --git a/stdlib/test/test/lux/lang/analysis/case.lux b/stdlib/test/test/lux/lang/analysis/case.lux new file mode 100644 index 000000000..9e775f8a3 --- /dev/null +++ b/stdlib/test/test/lux/lang/analysis/case.lux @@ -0,0 +1,194 @@ +(.module: + lux + (lux [io] + (control [monad #+ do] + pipe) + (data [bool "B/" Eq] + ["R" error] + [product] + [maybe] + [text "T/" Eq] + text/format + (coll [list "list/" Monad] + (set ["set" unordered]))) + ["r" math/random "r/" Monad] + [macro #+ Monad] + (macro [code]) + [lang] + (lang [type "type/" Eq] + (type ["tc" check]) + [".L" module] + (analysis [".A" type] + ["/" case])) + test) + (// ["_." primitive] + ["_." structure])) + +(def: (exhaustive-weaving branchings) + (-> (List (List Code)) (List (List Code))) + (case branchings + #.Nil + #.Nil + + (#.Cons head+ #.Nil) + (list/map (|>> list) head+) + + (#.Cons head+ tail++) + (do list.Monad + [tail+ (exhaustive-weaving tail++) + head head+] + (wrap (#.Cons head tail+))))) + +(def: #export (exhaustive-branches allow-literals? variantTC inputC) + (-> Bool (List [Code Code]) Code (r.Random (List Code))) + (case inputC + [_ (#.Bool _)] + (r/wrap (list (' true) (' false))) + + (^template [ ] + [_ ( _)] + (if allow-literals? + (do r.Monad + [?sample (r.maybe )] + (case ?sample + (#.Some sample) + (do @ + [else (exhaustive-branches allow-literals? variantTC inputC)] + (wrap (list& ( sample) else))) + + #.None + (wrap (list (' _))))) + (r/wrap (list (' _))))) + ([#.Nat r.nat code.nat] + [#.Int r.int code.int] + [#.Deg r.deg code.deg] + [#.Frac r.frac code.frac] + [#.Text (r.unicode +5) code.text]) + + (^ [_ (#.Tuple (list))]) + (r/wrap (list (' []))) + + (^ [_ (#.Record (list))]) + (r/wrap (list (' {}))) + + [_ (#.Tuple members)] + (do r.Monad + [member-wise-patterns (monad.map @ (exhaustive-branches allow-literals? variantTC) members)] + (wrap (|> member-wise-patterns + exhaustive-weaving + (list/map code.tuple)))) + + [_ (#.Record kvs)] + (do r.Monad + [#let [ks (list/map product.left kvs) + vs (list/map product.right kvs)] + member-wise-patterns (monad.map @ (exhaustive-branches allow-literals? variantTC) vs)] + (wrap (|> member-wise-patterns + exhaustive-weaving + (list/map (|>> (list.zip2 ks) code.record))))) + + (^ [_ (#.Form (list [_ (#.Tag _)] _))]) + (do r.Monad + [bundles (monad.map @ + (function (_ [_tag _code]) + (do @ + [v-branches (exhaustive-branches allow-literals? variantTC _code)] + (wrap (list/map (function (_ pattern) (` ((~ _tag) (~ pattern)))) + v-branches)))) + variantTC)] + (wrap (list/join bundles))) + + _ + (r/wrap (list)) + )) + +(def: #export (input variant-tags record-tags primitivesC) + (-> (List Code) (List Code) (List Code) (r.Random Code)) + (r.rec + (function (_ input) + ($_ r.either + (r/map product.right _primitive.primitive) + (do r.Monad + [choice (|> r.nat (:: @ map (n/% (list.size variant-tags)))) + #let [choiceT (maybe.assume (list.nth choice variant-tags)) + choiceC (maybe.assume (list.nth choice primitivesC))]] + (wrap (` ((~ choiceT) (~ choiceC))))) + (do r.Monad + [size (|> r.nat (:: @ map (n/% +3))) + elems (r.list size input)] + (wrap (code.tuple elems))) + (r/wrap (code.record (list.zip2 record-tags primitivesC))) + )))) + +(def: (branch body pattern) + (-> Code Code [Code Code]) + [pattern body]) + +(context: "Pattern-matching." + ## #seed +9253409297339902486 + ## #seed +3793366152923578600 + (<| (seed +5004137551292836565) + ## (times +100) + (do @ + [module-name (r.unicode +5) + variant-name (r.unicode +5) + record-name (|> (r.unicode +5) (r.filter (|>> (T/= variant-name) not))) + size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2)))) + variant-tags (|> (r.set text.Hash size (r.unicode +5)) (:: @ map set.to-list)) + record-tags (|> (r.set text.Hash size (r.unicode +5)) (:: @ map set.to-list)) + primitivesTC (r.list size _primitive.primitive) + #let [primitivesT (list/map product.left primitivesTC) + primitivesC (list/map product.right primitivesTC) + code-tag (|>> [module-name] code.tag) + variant-tags+ (list/map code-tag variant-tags) + record-tags+ (list/map code-tag record-tags) + variantTC (list.zip2 variant-tags+ primitivesC)] + inputC (input variant-tags+ record-tags+ primitivesC) + [outputT outputC] _primitive.primitive + [heterogeneousT heterogeneousC] (|> _primitive.primitive + (r.filter (|>> product.left (tc.checks? outputT) not))) + exhaustive-patterns (exhaustive-branches true variantTC inputC) + redundant-patterns (exhaustive-branches false variantTC inputC) + redundancy-idx (|> r.nat (:: @ map (n/% (list.size redundant-patterns)))) + heterogeneous-idx (|> r.nat (:: @ map (n/% (list.size exhaustive-patterns)))) + #let [exhaustive-branchesC (list/map (branch outputC) + exhaustive-patterns) + non-exhaustive-branchesC (list.take (dec (list.size exhaustive-branchesC)) + exhaustive-branchesC) + redundant-branchesC (<| (list/map (branch outputC)) + list.concat + (list (list.take redundancy-idx redundant-patterns) + (list (maybe.assume (list.nth redundancy-idx redundant-patterns))) + (list.drop redundancy-idx redundant-patterns))) + heterogeneous-branchesC (list.concat (list (list.take heterogeneous-idx exhaustive-branchesC) + (list (let [[_pattern _body] (maybe.assume (list.nth heterogeneous-idx exhaustive-branchesC))] + [_pattern heterogeneousC])) + (list.drop (inc heterogeneous-idx) exhaustive-branchesC))) + analyse-pm (|>> (/.case _primitive.analyse inputC) + (typeA.with-type outputT) + lang.with-scope + (do Monad + [_ (moduleL.declare-tags variant-tags false + (#.Named [module-name variant-name] + (type.variant primitivesT))) + _ (moduleL.declare-tags record-tags false + (#.Named [module-name record-name] + (type.tuple primitivesT)))]) + (moduleL.with-module +0 module-name))]] + ($_ seq + (test "Will reject empty pattern-matching (no branches)." + (|> (analyse-pm (list)) + _structure.check-fails)) + (test "Can analyse exhaustive pattern-matching." + (|> (analyse-pm exhaustive-branchesC) + _structure.check-succeeds)) + (test "Will reject non-exhaustive pattern-matching." + (|> (analyse-pm non-exhaustive-branchesC) + _structure.check-fails)) + (test "Will reject redundant pattern-matching." + (|> (analyse-pm redundant-branchesC) + _structure.check-fails)) + (test "Will reject pattern-matching if the bodies of the branches do not all have the same type." + (|> (analyse-pm heterogeneous-branchesC) + _structure.check-fails)) + )))) diff --git a/stdlib/test/test/lux/lang/analysis/primitive.lux b/stdlib/test/test/lux/lang/analysis/primitive.lux index ed9d8bfc6..8e4ca6dde 100644 --- a/stdlib/test/test/lux/lang/analysis/primitive.lux +++ b/stdlib/test/test/lux/lang/analysis/primitive.lux @@ -17,7 +17,7 @@ [".A" expression])) test)) -(def: analyse (expressionA.analyser (:! lang.Eval []))) +(def: #export analyse (expressionA.analyser (:! lang.Eval []))) (def: unit (r.Random Code) diff --git a/stdlib/test/test/lux/lang/analysis/structure.lux b/stdlib/test/test/lux/lang/analysis/structure.lux index ad6691287..20b911714 100644 --- a/stdlib/test/test/lux/lang/analysis/structure.lux +++ b/stdlib/test/test/lux/lang/analysis/structure.lux @@ -19,7 +19,7 @@ (type ["tc" check]) [".L" module] [".L" init] - [".L" analysis #+ Analysis] + [".L" analysis #+ Analysis Variant Tag] (analysis [".A" type] ["/" structure] [".A" expression])) @@ -43,7 +43,7 @@ ) (def: (check-sum' size tag variant) - (-> Nat analysisL.Tag analysisL.Variant Bool) + (-> Nat Tag (Variant Analysis) Bool) (let [variant-tag (if (get@ #analysisL.right? variant) (inc (get@ #analysisL.lefts variant)) (get@ #analysisL.lefts variant))] @@ -52,7 +52,7 @@ (and (n/= tag variant-tag))))) (def: (check-sum type size tag analysis) - (-> Type Nat analysisL.Tag (Meta Analysis) Bool) + (-> Type Nat Tag (Meta Analysis) Bool) (|> analysis (typeA.with-type type) (macro.run (initL.compiler [])) @@ -71,7 +71,7 @@ (moduleL.with-module +0 module))) (def: (check-variant module tags type size tag analysis) - (-> Text (List moduleL.Tag) Type Nat analysisL.Tag (Meta Analysis) Bool) + (-> Text (List moduleL.Tag) Type Nat Tag (Meta Analysis) Bool) (|> analysis (tagged module tags type) (typeA.with-type type) -- cgit v1.2.3