aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/analyser/case.lux
diff options
context:
space:
mode:
Diffstat (limited to 'new-luxc/source/luxc/analyser/case.lux')
-rw-r--r--new-luxc/source/luxc/analyser/case.lux260
1 files changed, 0 insertions, 260 deletions
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux
deleted file mode 100644
index 29256865a..000000000
--- a/new-luxc/source/luxc/analyser/case.lux
+++ /dev/null
@@ -1,260 +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>]))
- [meta]
- (meta [code]
- [type]
- (type ["tc" check])))
- (../.. ["&" base]
- (lang ["la" analysis])
- ["&;" scope])
- (.. ["&;" common]
- ["&;" structure])
- (. ["&&;" coverage]))
-
-(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<Meta>
- [? (&;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<Meta>
- [[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<Meta> wrap outputT)
-
- #;None
- (&;fail (format "Cannot apply type " (%type funcT) " to type " (%type inputT))))
-
- _
- (:: meta;Monad<Meta> 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<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
- (&;fail (format "Symbols must be unqualified inside patterns: " (%ident ident))))
-
- (^template [<type> <code-tag>]
- [cursor (<code-tag> test)]
- (&;with-cursor cursor
- (do meta;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 meta;Monad<Meta>
- [_ (&;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<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]))
- matches)]
- (wrap [(` ("lux case tuple" [(~@ memberP+)]))
- thenA])))
-
- _
- (&;fail (pattern-error inputT pattern))
- )))
-
- [cursor (#;Record record)]
- (do meta;Monad<Meta>
- [record (&structure;normalize record)
- [members recordT] (&structure;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<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 meta;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 meta;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)))))
-
- _
- (&;fail (pattern-error inputT pattern)))))
-
- (^ [cursor (#;Form (list& [_ (#;Tag tag)] values))])
- (&;with-cursor cursor
- (do meta;Monad<Meta>
- [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<Meta>
- [[inputT inputA] (&common;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 &&coverage;determine)
- outputTC (monad;map @ (|>. product;left &&coverage;determine) outputT)
- _ (case (monad;fold e;Monad<Error> &&coverage;merge outputHC outputTC)
- (#e;Success coverage)
- (if (&&coverage;exhaustive? coverage)
- (wrap [])
- (&;fail "Pattern-matching is not exhaustive."))
-
- (#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-11-05 14:12:26 +0000