(.module: lux (lux (control [monad #+ do] ["ex" exception #+ exception:]) (data [ident] [number] [product] [maybe] (coll [list "list/" Functor] [dict #+ Dict]) text/format) [macro] (macro [code]) (lang [type] (type ["tc" check]))) (luxc ["&" lang] (lang ["&." scope] ["&." module] ["la" analysis] (analysis ["&." common] ["&." inference])))) (exception: #export Invalid-Variant-Type) (exception: #export Invalid-Tuple-Type) (exception: #export Not-Quantified-Type) (exception: #export Cannot-Analyse-Variant) (exception: #export Cannot-Analyse-Tuple) (exception: #export Cannot-Infer-Numeric-Tag) (exception: #export Record-Keys-Must-Be-Tags) (exception: #export Cannot-Repeat-Tag) (exception: #export Tag-Does-Not-Belong-To-Record) (exception: #export Record-Size-Mismatch) (def: #export (analyse-sum analyse tag valueC) (-> &.Analyser Nat Code (Meta la.Analysis)) (do macro.Monad [expectedT macro.expected-type] (&.with-stacked-errors (function [_] (Cannot-Analyse-Variant (format " Type: " (%type expectedT) "\n" " Tag: " (%n tag) "\n" "Expression: " (%code valueC)))) (case expectedT (#.Sum _) (let [flat (type.flatten-variant expectedT) type-size (list.size flat)] (case (list.nth tag flat) (#.Some variant-type) (do @ [valueA (&.with-type variant-type (analyse valueC)) temp &scope.next-local] (wrap (la.sum tag type-size temp valueA))) #.None (&common.variant-out-of-bounds-error expectedT type-size tag))) (#.Named name unnamedT) (&.with-type unnamedT (analyse-sum analyse tag valueC)) (#.Var id) (do @ [?expectedT' (&.with-type-env (tc.read id))] (case ?expectedT' (#.Some expectedT') (&.with-type expectedT' (analyse-sum analyse tag valueC)) _ ## Cannot do inference when the tag is numeric. ## This is because there is no way of knowing how many ## cases the inferred sum type would have. (&.throw Cannot-Infer-Numeric-Tag (format " Type: " (%type expectedT) "\n" " Tag: " (%n tag) "\n" "Expression: " (%code valueC))) )) (^template [ ] ( _) (do @ [[instance-id instanceT] (&.with-type-env )] (&.with-type (maybe.assume (type.apply (list instanceT) expectedT)) (analyse-sum analyse tag valueC)))) ([#.UnivQ tc.existential] [#.ExQ tc.var]) (#.Apply inputT funT) (case funT (#.Var funT-id) (do @ [?funT' (&.with-type-env (tc.read funT-id))] (case ?funT' (#.Some funT') (&.with-type (#.Apply inputT funT') (analyse-sum analyse tag valueC)) _ (&.throw Invalid-Variant-Type (format " Type: " (%type expectedT) "\n" " Tag: " (%n tag) "\n" "Expression: " (%code valueC))))) _ (case (type.apply (list inputT) funT) #.None (&.throw Not-Quantified-Type (%type funT)) (#.Some outputT) (&.with-type outputT (analyse-sum analyse tag valueC)))) _ (&.throw Invalid-Variant-Type (format " Type: " (%type expectedT) "\n" " Tag: " (%n tag) "\n" "Expression: " (%code valueC))))))) (def: (analyse-typed-product analyse membersC+) (-> &.Analyser (List Code) (Meta la.Analysis)) (do macro.Monad [expectedT macro.expected-type] (loop [expectedT expectedT membersC+ membersC+] (case [expectedT membersC+] ## If the tuple runs out, whatever expression is the last gets ## matched to the remaining type. [tailT (#.Cons tailC #.Nil)] (&.with-type tailT (analyse tailC)) ## If the type and the code are still ongoing, match each ## sub-expression to its corresponding type. [(#.Product leftT rightT) (#.Cons leftC rightC)] (do @ [leftA (&.with-type leftT (analyse leftC)) rightA (recur rightT rightC)] (wrap (` [(~ leftA) (~ rightA)]))) ## If, however, the type runs out but there is still enough ## tail, the remaining elements get packaged into another ## tuple, and analysed through the intermediation of a ## temporary local variable. ## The reason for this is that it is assumed that the type of ## the tuple represents the expectations of the user. ## If the type is for a 3-tuple, but a 5-tuple is provided, it ## is assumed that the user intended the following layout: ## [0, 1, [2, 3, 4]] ## but that, for whatever reason, it was written in a flat ## way. ## The reason why an intermediate variable is used is that if ## the code was just re-written with just tuple nesting, the ## resulting analysis would have undone the explicity nesting, ## since Product nodes rely on nesting inherently, thereby ## blurring the line between what was wanted (the separation) ## and what was analysed. [tailT tailC] (do @ [g!tail (macro.gensym "tail")] (&.with-type tailT (analyse (` ("lux case" [(~+ tailC)] (~@ g!tail) (~@ g!tail)))))) )))) (def: #export (analyse-product analyse membersC) (-> &.Analyser (List Code) (Meta la.Analysis)) (do macro.Monad [expectedT macro.expected-type] (&.with-stacked-errors (function [_] (Cannot-Analyse-Tuple (format " Type: " (%type expectedT) "\n" "Expression: " (%code (` [(~+ membersC)]))))) (case expectedT (#.Product _) (analyse-typed-product analyse membersC) (#.Named name unnamedT) (&.with-type unnamedT (analyse-product analyse membersC)) (#.Var id) (do @ [?expectedT' (&.with-type-env (tc.read id))] (case ?expectedT' (#.Some expectedT') (&.with-type expectedT' (analyse-product analyse membersC)) _ ## Must do inference... (do @ [membersTA (monad.map @ (|>> analyse &common.with-unknown-type) membersC) _ (&.with-type-env (tc.check expectedT (type.tuple (list/map product.left membersTA))))] (wrap (la.product (list/map product.right membersTA)))))) (^template [ ] ( _) (do @ [[instance-id instanceT] (&.with-type-env )] (&.with-type (maybe.assume (type.apply (list instanceT) expectedT)) (analyse-product analyse membersC)))) ([#.UnivQ tc.existential] [#.ExQ tc.var]) (#.Apply inputT funT) (case funT (#.Var funT-id) (do @ [?funT' (&.with-type-env (tc.read funT-id))] (case ?funT' (#.Some funT') (&.with-type (#.Apply inputT funT') (analyse-product analyse membersC)) _ (&.throw Invalid-Tuple-Type (format " Type: " (%type expectedT) "\n" "Expression: " (%code (` [(~+ membersC)])))))) _ (case (type.apply (list inputT) funT) #.None (&.throw Not-Quantified-Type (%type funT)) (#.Some outputT) (&.with-type outputT (analyse-product analyse membersC)))) _ (&.throw Invalid-Tuple-Type (format " Type: " (%type expectedT) "\n" "Expression: " (%code (` [(~+ membersC)])))) )))) (def: #export (analyse-tagged-sum analyse tag valueC) (-> &.Analyser Ident Code (Meta la.Analysis)) (do macro.Monad [tag (macro.normalize tag) [idx group variantT] (macro.resolve-tag tag) expectedT macro.expected-type] (case expectedT (#.Var _) (do @ [#let [case-size (list.size group)] inferenceT (&inference.variant idx case-size variantT) [inferredT valueA+] (&inference.general analyse inferenceT (list valueC)) temp &scope.next-local] (wrap (la.sum idx case-size temp (|> valueA+ list.head maybe.assume)))) _ (analyse-sum analyse idx valueC)))) ## There cannot be any ambiguity or improper syntax when analysing ## records, so they must be normalized for further analysis. ## Normalization just means that all the tags get resolved to their ## canonical form (with their corresponding module identified). (def: #export (normalize record) (-> (List [Code Code]) (Meta (List [Ident Code]))) (monad.map macro.Monad (function [[key val]] (case key [_ (#.Tag key)] (do macro.Monad [key (macro.normalize key)] (wrap [key val])) _ (&.throw Record-Keys-Must-Be-Tags (format " Key: " (%code key) "\n" "Record: " (%code (code.record record)))))) record)) ## Lux already possesses the means to analyse tuples, so ## re-implementing the same functionality for records makes no sense. ## Records, thus, get transformed into tuples by ordering the elements. (def: #export (order record) (-> (List [Ident Code]) (Meta [(List Code) Type])) (case record ## empty-record = empty-tuple = unit = [] #.Nil (:: macro.Monad wrap [(list) Unit]) (#.Cons [head-k head-v] _) (do macro.Monad [head-k (macro.normalize head-k) [_ tag-set recordT] (macro.resolve-tag head-k) #let [size-record (list.size record) size-ts (list.size tag-set)] _ (if (n/= size-ts size-record) (wrap []) (&.throw Record-Size-Mismatch (format " Expected: " (|> size-ts nat-to-int %i) "\n" " Actual: " (|> size-record nat-to-int %i) "\n" " Type: " (%type recordT) "\n" "Expression: " (%code (|> record (list/map (function [[keyI valueC]] [(code.tag keyI) valueC])) code.record))))) #let [tuple-range (list.n/range +0 (n/dec size-ts)) tag->idx (dict.from-list ident.Hash (list.zip2 tag-set tuple-range))] idx->val (monad.fold @ (function [[key val] idx->val] (do @ [key (macro.normalize key)] (case (dict.get key tag->idx) #.None (&.throw Tag-Does-Not-Belong-To-Record (format " Tag: " (%code (code.tag key)) "\n" "Type: " (%type recordT))) (#.Some idx) (if (dict.contains? idx idx->val) (&.throw Cannot-Repeat-Tag (format " Tag: " (%code (code.tag key)) "\n" "Record: " (%code (code.record (list/map (function [[keyI valC]] [(code.tag keyI) valC]) record))))) (wrap (dict.put idx val idx->val)))))) (: (Dict Nat Code) (dict.new number.Hash)) record) #let [ordered-tuple (list/map (function [idx] (maybe.assume (dict.get idx idx->val))) tuple-range)]] (wrap [ordered-tuple recordT])) )) (def: #export (analyse-record analyse members) (-> &.Analyser (List [Code Code]) (Meta la.Analysis)) (do macro.Monad [members (normalize members) [membersC recordT] (order members)] (case membersC (^ (list singletonC)) (analyse singletonC) _ (do @ [expectedT macro.expected-type] (case expectedT (#.Var _) (do @ [inferenceT (&inference.record recordT) [inferredT membersA] (&inference.general analyse inferenceT membersC)] (wrap (la.product membersA))) _ (analyse-product analyse membersC))))))