From 15121222d570f8fe3c5a326208e4f0bad737e63c Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Tue, 31 Oct 2017 23:39:49 -0400 Subject: - Re-organized analysis. --- new-luxc/source/luxc/lang/analysis/case.lux | 260 ++++++++++++++++++++++++++++ 1 file changed, 260 insertions(+) create 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 new file mode 100644 index 000000000..1e40e38f1 --- /dev/null +++ b/new-luxc/source/luxc/lang/analysis/case.lux @@ -0,0 +1,260 @@ +(;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])) + [meta] + (meta [code] + [type] + (type ["tc" check]))) + (luxc ["&" base] + (lang ["la" analysis] + (analysis [";A" common] + [";A" structure] + (case [";A" coverage]))) + ["&;" scope])) + +(exception: #export Cannot-Match-Type-With-Pattern) +(exception: #export Sum-Type-Has-No-Case) +(exception: #export Unrecognized-Pattern-Syntax) +(exception: #export Cannot-Simplify-Type-For-Pattern-Matching) + +(def: (pattern-error type pattern) + (-> Type Code Text) + (Cannot-Match-Type-With-Pattern + (format " Type: " (%type type) "\n" + "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 (Meta Type)) + (case type + (#;Var id) + (do meta;Monad + [? (&;with-type-env + (tc;bound? id))] + (if ? + (do @ + [type' (&;with-type-env + (tc;read id))] + (simplify-case-type type')) + (&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type type)))) + + (#;Named name unnamedT) + (simplify-case-type unnamedT) + + (^or (#;UnivQ _) (#;ExQ _)) + (do meta;Monad + [[ex-id exT] (&;with-type-env + tc;existential)] + (simplify-case-type (maybe;assume (type;apply (list exT) type)))) + + (#;Apply inputT funcT) + (case (type;apply (list inputT) funcT) + (#;Some outputT) + (:: meta;Monad wrap outputT) + + #;None + (&;fail (format "Cannot apply type " (%type funcT) " to type " (%type inputT)))) + + _ + (:: meta;Monad 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 (Meta a) (Meta [la;Pattern a]))) + (case pattern + [cursor (#;Symbol ["" name])] + (&;with-cursor cursor + (do meta;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 + (&;fail (format "Symbols must be unqualified inside patterns: " (%ident ident)))) + + (^template [ ] + [cursor ( test)] + (&;with-cursor cursor + (do meta;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 meta;Monad + [_ (&;with-type-env + (tc;check inputT Unit)) + 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 meta;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])) + matches)] + (wrap [(` ("lux case tuple" [(~@ memberP+)])) + thenA]))) + + _ + (&;fail (pattern-error inputT pattern)) + ))) + + [cursor (#;Record record)] + (do meta;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 meta;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 meta;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 meta;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))))) + + _ + (&;fail (pattern-error inputT pattern))))) + + (^ [cursor (#;Form (list& [_ (#;Tag tag)] values))]) + (&;with-cursor cursor + (do meta;Monad + [tag (meta;normalize tag) + [idx group variantT] (meta;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 + (&;fail "Cannot have empty branches in pattern-matching expression.") + + (#;Cons [patternH bodyH] branchesT) + (do meta;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) + (if (coverageA;exhaustive? coverage) + (wrap []) + (&;fail "Pattern-matching is not exhaustive.")) + + (#e;Error error) + (&;fail error))] + (wrap (` ("lux case" (~ inputA) (~ (code;record (list& outputH outputT))))))))) -- cgit v1.2.3