aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/lang/analysis/case.lux
diff options
context:
space:
mode:
Diffstat (limited to 'new-luxc/source/luxc/lang/analysis/case.lux')
-rw-r--r--new-luxc/source/luxc/lang/analysis/case.lux312
1 files changed, 0 insertions, 312 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)))))))))
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-12 16:24:01 +0000