diff options
Diffstat (limited to 'new-luxc/source/luxc/lang/analysis')
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/case.lux | 312 | ||||
| -rw-r--r-- | new-luxc/source/luxc/lang/analysis/case/coverage.lux | 300 |
2 files changed, 0 insertions, 612 deletions
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<List> Monoid<List> Functor<List>])) - [macro] - (macro [code]) - (lang [type] - (type ["tc" check]))) - (luxc ["&" lang] - (lang ["&." scope] - ["la" analysis] - (analysis [".A" common] - [".A" structure] - (case [".A" coverage]))))) - -(do-template [<name>] - [(exception: #export (<name> {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<Meta> - [?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 [<tag> <instancer>] - ## (<tag> _) - ## (do macro.Monad<Meta> - ## [[_ instanceT] (&.with-type-env - ## <instancer>)] - ## (recur (maybe.assume (type.apply (list instanceT) caseT))))) - ## ([#.UnivQ tc.var] - ## [#.ExQ tc.existential]) - - (#.ExQ _) - (do macro.Monad<Meta> - [[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<Meta> - [funcT' (&.with-type-env - (do tc.Monad<Check> - [?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<Meta> wrap)) - - _ - (:: macro.Monad<Meta> 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<Meta> - [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 [<type> <code-tag>] - [cursor (<code-tag> test)] - (&.with-cursor cursor - (do macro.Monad<Meta> - [_ (&.with-type-env - (tc.check inputT <type>)) - 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<Meta> - [_ (&.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<Meta> - [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<Meta> - [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<Meta> - [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<Meta> - [[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<Meta> - [[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<Meta> - [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<Meta> - [[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<Error> 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<Bool>] - [number] - ["e" error "error/" Monad<Error>] - text/format - (coll [list "list/" Fold<List>] - (dictionary ["dict" unordered #+ Dict]))) - [macro "macro/" Monad<Meta>]) - (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<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 macro.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))))) |