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.lux260
1 files changed, 260 insertions, 0 deletions
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<List> Monoid<List> Functor<List>]))
+ [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<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 (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<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] (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)
+ (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)))))))))
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-23 23:46:17 +0000