(;module: lux (lux (control [monad #+ do] ["ex" exception #+ exception:] pipe) [function] (concurrency ["A" atom]) (data [ident] [number] [product] [maybe] (coll [list "list/" Functor] [dict #+ Dict]) [text] text/format) [meta] (meta [code] [type] (type ["tc" check]))) (luxc ["&" base] (lang ["la" analysis] (analysis ["&;" common] ["&;" inference])) ["&;" module] ["&;" scope])) (exception: #export Not-Variant-Type) (exception: #export Not-Tuple-Type) (exception: #export Not-Quantified-Type) (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 meta;Monad [expectedT meta;expected-type] (&;with-stacked-errors (function [_] (Not-Variant-Type (format " Type: " (%type expectedT) "\n" "Value: " (%code valueC) "\n" " Tag: " (%n tag)))) (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-expected-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-expected-type unnamedT (analyse-sum analyse tag valueC)) (#;Var id) (do @ [concrete? (&;with-type-env (tc;concrete? id))] (if concrete? (do @ [expectedT' (&;with-type-env (tc;read id))] (&;with-expected-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 " Tag: " (%n tag) "\n" "Value: " (%code valueC) "\n" " Type: " (%type expectedT))))) (^template [ ] ( _) (do @ [[instance-id instanceT] (&;with-type-env )] (&;with-expected-type (maybe;assume (type;apply (list instanceT) expectedT)) (analyse-sum analyse tag valueC)))) ([#;UnivQ tc;existential] [#;ExQ tc;var]) (#;Apply inputT funT) (case (type;apply (list inputT) funT) #;None (&;throw Not-Quantified-Type (%type funT)) (#;Some outputT) (&;with-expected-type outputT (analyse-sum analyse tag valueC))) _ (&;throw Not-Variant-Type (format " Type: " (%type expectedT) "\n" " Tag: " (%n tag) "\n" "Value: " (%code valueC))))))) (def: (analyse-typed-product analyse members) (-> &;Analyser (List Code) (Meta la;Analysis)) (do meta;Monad [expectedT meta;expected-type] (loop [expectedT expectedT members members] (case [expectedT members] ## 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-expected-type leftT (analyse leftC)) rightA (recur rightT rightC)] (wrap (` [(~ leftA) (~ rightA)]))) ## If the tuple runs out, whatever expression is the last gets ## matched to the remaining type. [tailT (#;Cons tailC #;Nil)] (&;with-expected-type tailT (analyse tailC)) ## 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 (meta;gensym "tail")] (&;with-expected-type tailT (analyse (` ((~' _lux_case) [(~@ tailC)] (~ g!tail) (~ g!tail)))))) )))) (def: #export (analyse-product analyse membersC) (-> &;Analyser (List Code) (Meta la;Analysis)) (do meta;Monad [expectedT meta;expected-type] (&;with-stacked-errors (function [_] (Not-Tuple-Type (format " Type: " (%type expectedT) "\n" "Value: " (%code (` [(~@ membersC)]))))) (case expectedT (#;Product _) (analyse-typed-product analyse membersC) (#;Named name unnamedT) (&;with-expected-type unnamedT (analyse-product analyse membersC)) (#;Var id) (do @ [concrete? (&;with-type-env (tc;concrete? id))] (if concrete? (do @ [expectedT' (&;with-type-env (tc;read id))] (&;with-expected-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-expected-type (maybe;assume (type;apply (list instanceT) expectedT)) (analyse-product analyse membersC)))) ([#;UnivQ tc;existential] [#;ExQ tc;var]) (#;Apply inputT funT) (case (type;apply (list inputT) funT) #;None (&;throw Not-Quantified-Type (%type funT)) (#;Some outputT) (&;with-expected-type outputT (analyse-product analyse membersC))) _ (&;throw Not-Tuple-Type (format " Type: " (%type expectedT) "\n" "Value: " (%code (` [(~@ membersC)])))) )))) (def: #export (analyse-tagged-sum analyse tag valueC) (-> &;Analyser Ident Code (Meta la;Analysis)) (do meta;Monad [tag (meta;normalize tag) [idx group variantT] (meta;resolve-tag tag) expectedT meta;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 meta;Monad (function [[key val]] (case key [_ (#;Tag key)] (do meta;Monad [key (meta;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 (:: meta;Monad wrap [(list) Unit]) (#;Cons [head-k head-v] _) (do meta;Monad [head-k (meta;normalize head-k) [_ tag-set recordT] (meta;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)))) #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 (meta;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 meta;Monad [members (normalize members) [membersC recordT] (order members) expectedT meta;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))))