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 ---------------------------- 1 file changed, 312 deletions(-) delete mode 100644 new-luxc/source/luxc/lang/analysis/case.lux (limited to 'new-luxc/source/luxc/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))))))))) -- cgit v1.2.3