aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/analyser.lux3
-rw-r--r--new-luxc/source/luxc/analyser/case.lux294
-rw-r--r--new-luxc/source/luxc/analyser/case/coverage.lux287
-rw-r--r--new-luxc/source/luxc/analyser/common.lux7
-rw-r--r--new-luxc/source/luxc/analyser/function.lux8
-rw-r--r--new-luxc/source/luxc/analyser/inference.lux109
-rw-r--r--new-luxc/source/luxc/analyser/procedure/common.lux3
-rw-r--r--new-luxc/source/luxc/analyser/structure.lux429
-rw-r--r--new-luxc/source/luxc/analyser/type.lux4
9 files changed, 644 insertions, 500 deletions
diff --git a/new-luxc/source/luxc/analyser.lux b/new-luxc/source/luxc/analyser.lux
index 44fa96081..e79b74f01 100644
--- a/new-luxc/source/luxc/analyser.lux
+++ b/new-luxc/source/luxc/analyser.lux
@@ -41,6 +41,8 @@
(: (-> Code (Lux la;Analysis))
(function analyse [ast]
(let [[cursor ast'] ast]
+ ## The cursor must be set in the compiler for the sake
+ ## of having useful error messages.
(&;with-cursor cursor
(case ast'
(^template [<tag> <analyser>]
@@ -57,6 +59,7 @@
(^ (#;Tuple (list)))
&&primitive;analyse-unit
+ ## Singleton tuples are equivalent to the element they contain.
(^ (#;Tuple (list singleton)))
(analyse singleton)
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux
index f3eec6b6b..306618caf 100644
--- a/new-luxc/source/luxc/analyser/case.lux
+++ b/new-luxc/source/luxc/analyser/case.lux
@@ -15,25 +15,25 @@
(macro [code])
[type]
(type ["TC" check]))
- (luxc ["&" base]
- (lang ["la" analysis])
- ["&;" env]
- (analyser ["&;" common]
- ["&;" structure])))
-
-(type: #rec Coverage
- #PartialC
- (#BoolC Bool)
- (#VariantC Nat (D;Dict Nat Coverage))
- (#SeqC Coverage Coverage)
- (#AltC Coverage Coverage)
- #TotalC)
+ (../.. ["&" base]
+ (lang ["la" analysis])
+ ["&;" env])
+ (.. ["&;" common]
+ ["&;" structure])
+ (. ["&&;" coverage]))
(def: (pattern-error type pattern)
(-> Type Code Text)
(format "Cannot match this type: " (%type type) "\n"
" With this 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 (Lux Type))
(case type
@@ -60,6 +60,22 @@
_
(:: Monad<Lux> 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 (Lux a) (Lux [la;Pattern a])))
(case pattern
@@ -143,10 +159,10 @@
(&;fail (pattern-error inputT pattern))
)))
- [cursor (#;Record pairs)]
+ [cursor (#;Record record)]
(do Monad<Lux>
- [pairs (&structure;normalize-record pairs)
- [members recordT] (&structure;order-record pairs)
+ [record (&structure;normalize record)
+ [members recordT] (&structure;order record)
_ (&;within-type-env
(TC;check inputT recordT))]
(analyse-pattern (#;Some (list;size members)) inputT [cursor (#;Tuple members)] next))
@@ -200,240 +216,6 @@
(&;fail (format "Unrecognized pattern syntax: " (%code pattern)))
))
-(def: (analyse-branch analyse inputT pattern body)
- (-> &;Analyser Type Code Code (Lux [la;Pattern la;Analysis]))
- (analyse-pattern #;None inputT pattern (analyse body)))
-
-(do-template [<name> <tag>]
- [(def: (<name> coverage)
- (-> Coverage Bool)
- (case coverage
- (<tag> _)
- true
-
- _
- false))]
-
- [total? #TotalC]
- [alt? #AltC]
- )
-
-(def: (determine-coverage pattern)
- (-> la;Pattern Coverage)
- (case pattern
- (^or (#la;BindP _) (^ (#la;TupleP (list))))
- #TotalC
-
- (^ (#la;TupleP (list singleton)))
- (determine-coverage singleton)
-
- (#la;BoolP value)
- (#BoolC value)
-
- (^or (#la;NatP _) (#la;IntP _) (#la;DegP _)
- (#la;RealP _) (#la;CharP _) (#la;TextP _))
- #PartialC
-
- (#la;TupleP subs)
- (loop [subs subs]
- (case subs
- #;Nil
- #TotalC
-
- (#;Cons sub subs')
- (let [post (recur subs')]
- (if (total? post)
- (determine-coverage sub)
- (#SeqC (determine-coverage sub)
- post)))))
-
- (#la;VariantP tag-id num-tags sub)
- (#VariantC num-tags
- (|> (D;new number;Hash<Nat>)
- (D;put tag-id (determine-coverage sub))))))
-
-(def: (xor left right)
- (-> Bool Bool Bool)
- (or (and left (not right))
- (and (not left) right)))
-
-(def: redundant-pattern
- (R;Result Coverage)
- (R;fail "Redundant pattern."))
-
-(def: (flatten-alt coverage)
- (-> Coverage (List Coverage))
- (case coverage
- (#AltC left right)
- (list& left (flatten-alt right))
-
- _
- (list coverage)))
-
-(struct: _ (Eq Coverage)
- (def: (= reference sample)
- (case [reference sample]
- [#TotalC #TotalC]
- true
-
- [(#BoolC sideR) (#BoolC sideS)]
- (B/= sideR sideS)
-
- [(#VariantC allR casesR) (#VariantC allS casesS)]
- (and (n.= allR allS)
- (:: (D;Eq<Dict> =) = casesR casesS))
-
- [(#SeqC leftR rightR) (#SeqC leftS rightS)]
- (and (= leftR leftS)
- (= rightR rightS))
-
- [(#AltC _) (#AltC _)]
- (let [flatR (flatten-alt reference)
- flatS (flatten-alt sample)]
- (and (n.= (list;size flatR) (list;size flatS))
- (list;every? (function [[coverageR coverageS]]
- (= coverageR coverageS))
- (list;zip2 flatR flatS))))
-
- _
- false)))
-
-(open Eq<Coverage> "C/")
-
-(def: (merge-coverages addition so-far)
- (-> Coverage Coverage (R;Result Coverage))
- (case [addition so-far]
- ## The addition cannot possibly improve the coverage.
- [_ #TotalC]
- redundant-pattern
-
- ## The addition completes the coverage.
- [#TotalC _]
- (R/wrap #TotalC)
-
- [#PartialC #PartialC]
- (R/wrap #PartialC)
-
- (^multi [(#BoolC sideA) (#BoolC sideSF)]
- (xor sideA sideSF))
- (R/wrap #TotalC)
-
- [(#VariantC allA casesA) (#VariantC allSF casesSF)]
- (cond (not (n.= allSF allA))
- (R;fail "Variants do not match.")
-
- (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA)
- redundant-pattern
-
- ## else
- (do R;Monad<Result>
- [casesM (foldM @
- (function [[tagA coverageA] casesSF']
- (case (D;get tagA casesSF')
- (#;Some coverageSF)
- (do @
- [coverageM (merge-coverages coverageA coverageSF)]
- (wrap (D;put tagA coverageM casesSF')))
-
- #;None
- (wrap (D;put tagA coverageA casesSF'))))
- casesSF (D;entries casesA))]
- (wrap (if (let [case-coverages (D;values casesM)]
- (and (n.= allSF (list;size case-coverages))
- (list;every? total? case-coverages)))
- #TotalC
- (#VariantC allSF casesM)))))
-
- [(#SeqC leftA rightA) (#SeqC leftSF rightSF)]
- (case [(C/= leftSF leftA) (C/= rightSF rightA)]
- ## There is nothing the addition adds to the coverage.
- [true true]
- redundant-pattern
-
- ## The 2 sequences cannot possibly be merged.
- [false false]
- (R/wrap (#AltC so-far addition))
-
- ## Same prefix
- [true false]
- (do R;Monad<Result>
- [rightM (merge-coverages rightA rightSF)]
- (if (total? rightM)
- (wrap leftSF)
- (wrap (#SeqC leftSF rightM))))
-
- ## Same suffix
- [false true]
- (do R;Monad<Result>
- [leftM (merge-coverages leftA leftSF)]
- (wrap (#SeqC leftM rightA))))
-
- ## The left part will always match, so the addition is redundant.
- (^multi [(#SeqC left right) single]
- (C/= left single))
- redundant-pattern
-
- ## The right part is not necessary, since it can always match the left.
- (^multi [single (#SeqC left right)]
- (C/= left single))
- (R/wrap single)
-
- [_ (#AltC leftS rightS)]
- (do R;Monad<Result>
- [#let [fuse-once (: (-> Coverage (List Coverage)
- (R;Result [(Maybe Coverage)
- (List Coverage)]))
- (function [coverage possibilities]
- (loop [alts possibilities]
- (case alts
- #;Nil
- (wrap [#;None (list coverage)])
-
- (#;Cons alt alts')
- (case (merge-coverages coverage alt)
- (#R;Success altM)
- (case altM
- (#AltC _)
- (do @
- [[success alts+] (recur alts')]
- (wrap [success (#;Cons alt alts+)]))
-
- _
- (wrap [(#;Some altM) alts']))
-
- (#R;Error error)
- (R;fail error))
- ))))]
- [success possibilities] (fuse-once addition (flatten-alt so-far))]
- (loop [success success
- possibilities possibilities]
- (case success
- (#;Some coverage')
- (do @
- [[success' possibilities'] (fuse-once coverage' possibilities)]
- (recur success' possibilities'))
-
- #;None
- (case (list;reverse possibilities)
- #;Nil
- (R;fail "{ This is not supposed to happen... }")
-
- (#;Cons last prevs)
- (wrap (L/fold (function [left right] (#AltC left right))
- last
- prevs))))))
-
- _
- (if (C/= so-far addition)
- ## The addition cannot possibly improve the coverage.
- redundant-pattern
- ## There are now 2 alternative paths.
- (R/wrap (#AltC so-far addition)))))
-
-(def: get-coverage
- (-> [la;Pattern la;Analysis] Coverage)
- (|>. product;left determine-coverage))
-
(def: #export (analyse-case analyse input branches)
(-> &;Analyser Code (List [Code Code]) (Lux la;Analysis))
(case branches
@@ -444,17 +226,17 @@
(do Monad<Lux>
[[inputT inputA] (&common;with-unknown-type
(analyse input))
- outputH (analyse-branch analyse inputT patternH bodyH)
+ outputH (analyse-pattern #;None inputT patternH (analyse bodyH))
outputT (mapM @
(function [[patternT bodyT]]
- (analyse-branch analyse inputT patternT bodyT))
+ (analyse-pattern #;None inputT patternT (analyse bodyT)))
branchesT)
_ (case (foldM R;Monad<Result>
- merge-coverages
- (get-coverage outputH)
- (L/map get-coverage outputT))
+ &&coverage;merge
+ (|> outputH product;left &&coverage;determine)
+ (L/map (|>. product;left &&coverage;determine) outputT))
(#R;Success coverage)
- (if (total? coverage)
+ (if (&&coverage;total? coverage)
(wrap [])
(&;fail "Pattern-matching is not total."))
diff --git a/new-luxc/source/luxc/analyser/case/coverage.lux b/new-luxc/source/luxc/analyser/case/coverage.lux
new file mode 100644
index 000000000..754e555b2
--- /dev/null
+++ b/new-luxc/source/luxc/analyser/case/coverage.lux
@@ -0,0 +1,287 @@
+(;module:
+ lux
+ (lux (control monad
+ eq)
+ (data [bool "B/" Eq<Bool>]
+ [number]
+ ["R" result "R/" Monad<Result>]
+ (coll [list "L/" Fold<List>]
+ ["D" dict])))
+ (luxc (lang ["la" analysis])))
+
+## The coverage of a pattern-matching expression summarizes how well
+## all the possible values of an input are being covered by the
+## different patterns involved.
+## Ideally, the pattern-matching has "total" coverage, which just
+## means that every possible value can be matched by at least 1
+## pattern.
+## Every other coverage is considered partial, and it would be valued
+## as insuficient (since it could lead to runtime errors due to values
+## not being handled by any pattern).
+## The #Partial tag covers arbitrary partial coverages in a general
+## way, while the other tags cover more specific cases for booleans
+## and variants.
+(type: #export #rec Coverage
+ #Partial
+ (#Bool Bool)
+ (#Variant Nat (D;Dict Nat Coverage))
+ (#Seq Coverage Coverage)
+ (#Alt Coverage Coverage)
+ #Total)
+
+(def: #export (total? coverage)
+ (-> Coverage Bool)
+ (case coverage
+ (#Total _)
+ true
+
+ _
+ false))
+
+(def: #export (determine pattern)
+ (-> la;Pattern Coverage)
+ (case pattern
+ ## Binding amounts to total coverage because any value can be
+ ## matched that way.
+ ## Unit [] amounts to total coverage because there is only one
+ ## possible value, so matching against it covers all cases.
+ (^or (#la;BindP _) (^ (#la;TupleP (list))))
+ #Total
+
+ (^ (#la;TupleP (list singleton)))
+ (determine singleton)
+
+ ## Primitive patterns always have partial coverage because there
+ ## are too many possibilities as far as values go.
+ (^or (#la;NatP _) (#la;IntP _) (#la;DegP _)
+ (#la;RealP _) (#la;CharP _) (#la;TextP _))
+ #Partial
+
+ ## Bools are the exception, since there is only "true" and
+ ## "false", which means it is possible for boolean
+ ## pattern-matching to become total if complementary parts meet.
+ (#la;BoolP value)
+ (#Bool value)
+
+ ## Tuple patterns can be total if there is totality for all of
+ ## their sub-patterns.
+ (#la;TupleP subs)
+ (loop [subs subs]
+ (case subs
+ #;Nil
+ #Total
+
+ (#;Cons sub subs')
+ (let [post (recur subs')]
+ (if (total? post)
+ (determine sub)
+ (#Seq (determine sub)
+ post)))))
+
+ ## Variant patterns can be shown to be total if all the possible
+ ## cases are handled totally.
+ (#la;VariantP tag-id num-tags sub)
+ (#Variant num-tags
+ (|> (D;new number;Hash<Nat>)
+ (D;put tag-id (determine sub))))))
+
+(def: (xor left right)
+ (-> Bool Bool Bool)
+ (or (and left (not right))
+ (and (not left) right)))
+
+## The coverage checker not only verifies that pattern-matching is
+## total, but also that there are no redundant patterns.
+## Redundant patterns will never be executed, since there will
+## always be a pattern prior to them that would match the input.
+## Because of that, the presence of redundant patterns is assumed to
+## be a bug, likely due to programmer carelessness.
+(def: redundant-pattern
+ (R;Result Coverage)
+ (R;fail "Redundant pattern."))
+
+(def: (flatten-alt coverage)
+ (-> Coverage (List Coverage))
+ (case coverage
+ (#Alt left right)
+ (list& left (flatten-alt right))
+
+ _
+ (list coverage)))
+
+(struct: _ (Eq Coverage)
+ (def: (= reference sample)
+ (case [reference sample]
+ [#Total #Total]
+ true
+
+ [(#Bool sideR) (#Bool sideS)]
+ (B/= sideR sideS)
+
+ [(#Variant allR casesR) (#Variant allS casesS)]
+ (and (n.= allR allS)
+ (:: (D;Eq<Dict> =) = casesR casesS))
+
+ [(#Seq leftR rightR) (#Seq leftS rightS)]
+ (and (= leftR leftS)
+ (= rightR rightS))
+
+ [(#Alt _) (#Alt _)]
+ (let [flatR (flatten-alt reference)
+ flatS (flatten-alt sample)]
+ (and (n.= (list;size flatR) (list;size flatS))
+ (list;every? (function [[coverageR coverageS]]
+ (= coverageR coverageS))
+ (list;zip2 flatR flatS))))
+
+ _
+ false)))
+
+(open Eq<Coverage> "C/")
+
+## After determining the coverage of each individual pattern, it is
+## necessary to merge them all to figure out if the entire
+## pattern-matching expression is total and whether it contains
+## redundant patterns.
+(def: #export (merge addition so-far)
+ (-> Coverage Coverage (R;Result Coverage))
+ (case [addition so-far]
+ ## The addition cannot possibly improve the coverage.
+ [_ #Total]
+ redundant-pattern
+
+ ## The addition completes the coverage.
+ [#Total _]
+ (R/wrap #Total)
+
+ [#Partial #Partial]
+ (R/wrap #Partial)
+
+ ## 2 boolean coverages are total if they compliment one another.
+ (^multi [(#Bool sideA) (#Bool sideSF)]
+ (xor sideA sideSF))
+ (R/wrap #Total)
+
+ [(#Variant allA casesA) (#Variant allSF casesSF)]
+ (cond (not (n.= allSF allA))
+ (R;fail "Variants do not match.")
+
+ (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA)
+ redundant-pattern
+
+ ## else
+ (do R;Monad<Result>
+ [casesM (foldM @
+ (function [[tagA coverageA] casesSF']
+ (case (D;get tagA casesSF')
+ (#;Some coverageSF)
+ (do @
+ [coverageM (merge coverageA coverageSF)]
+ (wrap (D;put tagA coverageM casesSF')))
+
+ #;None
+ (wrap (D;put tagA coverageA casesSF'))))
+ casesSF (D;entries casesA))]
+ (wrap (if (let [case-coverages (D;values casesM)]
+ (and (n.= allSF (list;size case-coverages))
+ (list;every? total? case-coverages)))
+ #Total
+ (#Variant allSF casesM)))))
+
+ [(#Seq leftA rightA) (#Seq leftSF rightSF)]
+ (case [(C/= leftSF leftA) (C/= rightSF rightA)]
+ ## There is nothing the addition adds to the coverage.
+ [true true]
+ redundant-pattern
+
+ ## The 2 sequences cannot possibly be merged.
+ [false false]
+ (R/wrap (#Alt so-far addition))
+
+ ## Same prefix
+ [true false]
+ (do R;Monad<Result>
+ [rightM (merge rightA rightSF)]
+ (if (total? rightM)
+ ## If all that follows is total, then it can be safely dropped
+ ## (since only the "left" part would influence whether the
+ ## merged coverage is total or not).
+ (wrap leftSF)
+ (wrap (#Seq leftSF rightM))))
+
+ ## Same suffix
+ [false true]
+ (do R;Monad<Result>
+ [leftM (merge leftA leftSF)]
+ (wrap (#Seq leftM rightA))))
+
+ ## The left part will always match, so the addition is redundant.
+ (^multi [(#Seq left right) single]
+ (C/= left single))
+ redundant-pattern
+
+ ## The right part is not necessary, since it can always match the left.
+ (^multi [single (#Seq left right)]
+ (C/= left single))
+ (R/wrap single)
+
+ ## When merging a new coverage against one based on Alt, it may be
+ ## that one of the many coverages in the Alt is complementary to
+ ## the new one, so effort must be made to fuse carefully, to match
+ ## the right coverages together.
+ ## If one of the Alt sub-coverages matches the new one, the cycle
+ ## must be repeated, in case the resulting coverage can now match
+ ## other ones in the original Alt.
+ ## This process must be repeated until no further productive
+ ## merges can be done.
+ [_ (#Alt leftS rightS)]
+ (do R;Monad<Result>
+ [#let [fuse-once (: (-> Coverage (List Coverage)
+ (R;Result [(Maybe Coverage)
+ (List Coverage)]))
+ (function [coverage possibilities]
+ (loop [alts possibilities]
+ (case alts
+ #;Nil
+ (wrap [#;None (list coverage)])
+
+ (#;Cons alt alts')
+ (case (merge coverage alt)
+ (#R;Success altM)
+ (case altM
+ (#Alt _)
+ (do @
+ [[success alts+] (recur alts')]
+ (wrap [success (#;Cons alt alts+)]))
+
+ _
+ (wrap [(#;Some altM) alts']))
+
+ (#R;Error error)
+ (R;fail error))
+ ))))]
+ [success possibilities] (fuse-once addition (flatten-alt so-far))]
+ (loop [success success
+ possibilities possibilities]
+ (case success
+ (#;Some coverage')
+ (do @
+ [[success' possibilities'] (fuse-once coverage' possibilities)]
+ (recur success' possibilities'))
+
+ #;None
+ (case (list;reverse possibilities)
+ #;Nil
+ (R;fail "{ This is not supposed to happen... }")
+
+ (#;Cons last prevs)
+ (wrap (L/fold (function [left right] (#Alt left right))
+ last
+ prevs))))))
+
+ _
+ (if (C/= so-far addition)
+ ## The addition cannot possibly improve the coverage.
+ redundant-pattern
+ ## There are now 2 alternative paths.
+ (R/wrap (#Alt so-far addition)))))
diff --git a/new-luxc/source/luxc/analyser/common.lux b/new-luxc/source/luxc/analyser/common.lux
index 7a9e5dbf8..c1246d81c 100644
--- a/new-luxc/source/luxc/analyser/common.lux
+++ b/new-luxc/source/luxc/analyser/common.lux
@@ -30,3 +30,10 @@
output (body [id var])
_ (&;within-type-env (TC;delete-var id))]
(wrap output)))
+
+(def: #export (variant-out-of-bounds-error type size tag)
+ (All [a] (-> Type Nat Nat (Lux a)))
+ (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n"
+ " Tag: " (%i (nat-to-int tag)) "\n"
+ "Size: " (%i (nat-to-int size)) "\n"
+ "Type: " (%type type))))
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 394e65c4d..1aad8954e 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -62,7 +62,7 @@
(function [[output-id outputT]]
(do @
[#let [funT (#;Function inputT outputT)]
- =function (recur funT)
+ funA (recur funT)
funT' (&;within-type-env
(TC;clean output-id funT))
concrete-input? (&;within-type-env
@@ -70,15 +70,17 @@
funT'' (if concrete-input?
(&;within-type-env
(TC;clean input-id funT'))
- (wrap (#;UnivQ (list) (&inference;bind-var input-id +1 funT'))))
+ (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
_ (&;within-type-env
(TC;check expected funT''))]
- (wrap =function))
+ (wrap funA))
))))))
(#;Function inputT outputT)
(<| (:: @ map (|>. #la;Function))
&;with-scope
+ ## Functions have access not only to their argument, but
+ ## also to themselves, through a local variable.
(&env;with-local [func-name functionT])
(&env;with-local [arg-name inputT])
(&;with-expected-type outputT)
diff --git a/new-luxc/source/luxc/analyser/inference.lux b/new-luxc/source/luxc/analyser/inference.lux
index 824071ab3..11ec58eb3 100644
--- a/new-luxc/source/luxc/analyser/inference.lux
+++ b/new-luxc/source/luxc/analyser/inference.lux
@@ -10,16 +10,24 @@
(lang ["la" analysis #+ Analysis])
(analyser ["&;" common])))
-(def: #export (bind-var var-id bound-idx type)
+## When doing inference, type-variables often need to be created in
+## order to figure out which types are present in the expression being
+## inferred.
+## If a type-variable never gets bound/resolved to a type, then that
+## means the expression can be generalized through universal
+## quantification.
+## When that happens, the type-variable must be replaced by an
+## argument to the universally-quantified type.
+(def: #export (replace-var var-id bound-idx type)
(-> Nat Nat Type Type)
(case type
(#;Host name params)
- (#;Host name (L/map (bind-var var-id bound-idx) params))
+ (#;Host name (L/map (replace-var var-id bound-idx) params))
(^template [<tag>]
(<tag> left right)
- (<tag> (bind-var var-id bound-idx left)
- (bind-var var-id bound-idx right)))
+ (<tag> (replace-var var-id bound-idx left)
+ (replace-var var-id bound-idx right)))
([#;Sum]
[#;Product]
[#;Function]
@@ -32,18 +40,25 @@
(^template [<tag>]
(<tag> env quantified)
- (<tag> (L/map (bind-var var-id bound-idx) env)
- (bind-var var-id (n.+ +2 bound-idx) quantified)))
+ (<tag> (L/map (replace-var var-id bound-idx) env)
+ (replace-var var-id (n.+ +2 bound-idx) quantified)))
([#;UnivQ]
[#;ExQ])
(#;Named name unnamedT)
(#;Named name
- (bind-var var-id bound-idx unnamedT))
+ (replace-var var-id bound-idx unnamedT))
_
type))
+## Type-inference works by applying some (potentially quantified) type
+## to a sequence of values.
+## Function types are used for this, although inference is not always
+## done for function application (alternative uses may be records and
+## tagged variants).
+## But, so long as the type being used for the inference can be trated
+## as a function type, this method of inference should work.
(def: #export (apply-function analyse funcT args)
(-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
(case args
@@ -63,10 +78,12 @@
(do @
[? (&;within-type-env
(TC;bound? var-id))
+ ## Quantify over the type if genericity/parametricity
+ ## is discovered.
outputT' (if ?
(&;within-type-env
(TC;clean var-id outputT))
- (wrap (#;UnivQ (list) (bind-var var-id +1 outputT))))]
+ (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))]
(wrap [outputT' argsA])))))
(#;ExQ _)
@@ -75,6 +92,13 @@
TC;existential)]
(apply-function analyse (assume (type;apply-type funcT exT)) args))
+ ## Arguments are inferred back-to-front because, by convention,
+ ## Lux functions take the most important arguments *last*, which
+ ## means that the most information for doing proper inference is
+ ## located in the last arguments to a function call.
+ ## By inferring back-to-front, a lot of type-annotations can be
+ ## avoided in Lux code, since the inference algorithm can piece
+ ## things together more easily.
(#;Function inputT outputT)
(do Monad<Lux>
[[outputT' args'A] (apply-function analyse outputT args')
@@ -88,3 +112,72 @@
_
(&;fail (format "Cannot apply a non-function: " (%type funcT))))
))
+
+## Turns a record type into the kind of function type suitable for inference.
+(def: #export (record-inference-type type)
+ (-> Type (Lux Type))
+ (case type
+ (#;Named name unnamedT)
+ (do Monad<Lux>
+ [unnamedT+ (record-inference-type unnamedT)]
+ (wrap (#;Named name unnamedT+)))
+
+ (^template [<tag>]
+ (<tag> env bodyT)
+ (do Monad<Lux>
+ [bodyT+ (record-inference-type bodyT)]
+ (wrap (<tag> env bodyT+))))
+ ([#;UnivQ]
+ [#;ExQ])
+
+ (#;Product _)
+ (:: Monad<Lux> wrap (type;function (type;flatten-tuple type) type))
+
+ _
+ (&;fail (format "Not a record type: " (%type type)))))
+
+## Turns a variant type into the kind of function type suitable for inference.
+(def: #export (variant-inference-type tag expected-size type)
+ (-> Nat Nat Type (Lux Type))
+ (case type
+ (#;Named name unnamedT)
+ (do Monad<Lux>
+ [unnamedT+ (variant-inference-type tag expected-size unnamedT)]
+ (wrap (#;Named name unnamedT+)))
+
+ (^template [<tag>]
+ (<tag> env bodyT)
+ (do Monad<Lux>
+ [bodyT+ (variant-inference-type tag expected-size bodyT)]
+ (wrap (<tag> env bodyT+))))
+ ([#;UnivQ]
+ [#;ExQ])
+
+ (#;Sum _)
+ (let [cases (type;flatten-variant type)
+ actual-size (list;size cases)
+ boundary (n.dec expected-size)]
+ (cond (or (n.= expected-size actual-size)
+ (and (n.> expected-size actual-size)
+ (n.< boundary tag)))
+ (case (list;nth tag cases)
+ (#;Some caseT)
+ (:: Monad<Lux> wrap (type;function (list caseT) type))
+
+ #;None
+ (&common;variant-out-of-bounds-error type expected-size tag))
+
+ (n.< expected-size actual-size)
+ (&;fail (format "Variant type is smaller than expected." "\n"
+ "Expected: " (%i (nat-to-int expected-size)) "\n"
+ " Actual: " (%i (nat-to-int actual-size))))
+
+ (n.= boundary tag)
+ (let [caseT (type;variant (list;drop boundary cases))]
+ (:: Monad<Lux> wrap (type;function (list caseT) type)))
+
+ ## else
+ (&common;variant-out-of-bounds-error type expected-size tag)))
+
+ _
+ (&;fail (format "Not a variant type: " (%type type)))))
diff --git a/new-luxc/source/luxc/analyser/procedure/common.lux b/new-luxc/source/luxc/analyser/procedure/common.lux
index 8a03f9cad..303cdc61c 100644
--- a/new-luxc/source/luxc/analyser/procedure/common.lux
+++ b/new-luxc/source/luxc/analyser/procedure/common.lux
@@ -71,6 +71,7 @@
(simple-proc proc (list fromT) toT))
## [Analysers]
+## "lux is" represents reference/pointer equality.
(def: (analyse-lux-is proc)
(-> Text Proc-Analyser)
(function [analyse args]
@@ -79,6 +80,8 @@
((binary-operation varT varT Bool proc)
analyse args)))))
+## "lux try" provides a simple way to interact with the host platform's
+## error-handling facilities.
(def: (analyse-lux-try proc)
(-> Text Proc-Analyser)
(function [analyse args]
diff --git a/new-luxc/source/luxc/analyser/structure.lux b/new-luxc/source/luxc/analyser/structure.lux
index 9447ea059..f93534463 100644
--- a/new-luxc/source/luxc/analyser/structure.lux
+++ b/new-luxc/source/luxc/analyser/structure.lux
@@ -24,7 +24,109 @@
(analyser ["&;" common]
["&;" inference])))
-## [Analysers]
+## Variants get analysed as binary sum types for the sake of semantic
+## simplicity.
+## This is because you can encode a variant of any size using just
+## binary sums by nesting them.
+
+(do-template [<name> <side>]
+ [(def: (<name> inner)
+ (-> la;Analysis la;Analysis)
+ (#la;Sum (<side> inner)))]
+
+ [sum-left #;Left]
+ [sum-right #;Right])
+
+(def: (variant tag size temp value)
+ (-> Nat Nat Nat la;Analysis la;Analysis)
+ (if (n.= (n.dec size) tag)
+ (if (n.= +1 tag)
+ (sum-right value)
+ (L/fold (function;const sum-left)
+ (sum-right value)
+ (list;n.range +0 (n.- +2 tag))))
+ (L/fold (function;const sum-left)
+ (case value
+ (#la;Sum _)
+ (#la;Case value (list [(#la;BindP temp)
+ (#la;Relative (#;Local temp))]))
+
+ _
+ value)
+ (list;n.range +0 tag))))
+
+(def: #export (analyse-sum analyse tag valueC)
+ (-> &;Analyser Nat Code (Lux la;Analysis))
+ (do Monad<Lux>
+ [expected macro;expected-type]
+ (&;with-stacked-errors
+ (function [_] (format "Invalid type for variant: " (%type expected)))
+ (case expected
+ (#;Sum _)
+ (let [flat (type;flatten-variant expected)
+ type-size (list;size flat)]
+ (case (list;nth tag flat)
+ (#;Some variant-type)
+ (do @
+ [valueA (&;with-expected-type variant-type
+ (analyse valueC))
+ temp &env;next-local]
+ (wrap (variant tag type-size temp valueA)))
+
+ #;None
+ (&common;variant-out-of-bounds-error expected type-size tag)))
+
+ (#;Named name unnamedT)
+ (&;with-expected-type unnamedT
+ (analyse-sum analyse tag valueC))
+
+ (#;Var id)
+ (do @
+ [bound? (&;within-type-env
+ (TC;bound? id))]
+ (if bound?
+ (do @
+ [expected' (&;within-type-env
+ (TC;read-var id))]
+ (&;with-expected-type expected'
+ (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.
+ (&;fail (format "Invalid type for variant: " (%type expected)))))
+
+ (#;UnivQ _)
+ (do @
+ [[var-id var] (&;within-type-env
+ TC;existential)]
+ (&;with-expected-type (assume (type;apply-type expected var))
+ (analyse-sum analyse tag valueC)))
+
+ (#;ExQ _)
+ (&common;with-var
+ (function [[var-id var]]
+ (&;with-expected-type (assume (type;apply-type expected var))
+ (analyse-sum analyse tag valueC))))
+
+ _
+ (&;fail "")))))
+
+## Tuples get analysed into binary products for the sake of semantic
+## simplicity, since products/pairs can encode tuples of any length
+## through nesting.
+
+(def: (product members)
+ (-> (List la;Analysis) la;Analysis)
+ (case members
+ #;Nil
+ #la;Unit
+
+ (#;Cons singleton #;Nil)
+ singleton
+
+ (#;Cons left right)
+ (#la;Product left (product right))))
+
(def: (analyse-typed-product analyse members)
(-> &;Analyser (List Code) (Lux la;Analysis))
(do Monad<Lux>
@@ -32,6 +134,8 @@
(loop [expected expected
members members]
(case [expected 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
@@ -39,10 +143,29 @@
rightA (recur rightT rightC)]
(wrap (#la;Product 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 (macro;gensym "tail")]
@@ -52,73 +175,6 @@
(~ g!tail))))))
))))
-(def: #export (normalize-record pairs)
- (-> (List [Code Code]) (Lux (List [Ident Code])))
- (mapM Monad<Lux>
- (function [[key val]]
- (case key
- [_ (#;Tag key)]
- (do Monad<Lux>
- [key (macro;normalize key)]
- (wrap [key val]))
-
- _
- (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key)))))
- pairs))
-
-(def: #export (order-record pairs)
- (-> (List [Ident Code]) (Lux [(List Code) Type]))
- (case pairs
- (#;Cons [head-k head-v] _)
- (do Monad<Lux>
- [head-k (macro;normalize head-k)
- [_ tag-set recordT] (macro;resolve-tag head-k)
- #let [size-record (list;size pairs)
- size-ts (list;size tag-set)]
- _ (if (n.= size-ts size-record)
- (wrap [])
- (&;fail (format "Record size does not match tag-set size." "\n"
- "Expected: " (|> size-ts nat-to-int %i) "\n"
- " Actual: " (|> size-record nat-to-int %i) "\n"
- "For type: " (%type recordT))))
- #let [tuple-range (list;n.range +0 (n.dec size-ts))
- tag->idx (D;from-list ident;Hash<Ident> (list;zip2 tag-set tuple-range))]
- idx->val (foldM @
- (function [[key val] idx->val]
- (do @
- [key (macro;normalize key)]
- (case (D;get key tag->idx)
- #;None
- (&;fail (format "Tag " (%code (code;tag key))
- " does not belong to tag-set for type " (%type recordT)))
-
- (#;Some idx)
- (if (D;contains? idx idx->val)
- (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
- (wrap (D;put idx val idx->val))))))
- (: (D;Dict Nat Code)
- (D;new number;Hash<Nat>))
- pairs)
- #let [ordered-tuple (L/map (function [idx]
- (assume (D;get idx idx->val)))
- tuple-range)]]
- (wrap [ordered-tuple recordT]))
-
- _
- (:: Monad<Lux> wrap [(list) Unit])))
-
-(def: (tuple members)
- (-> (List la;Analysis) la;Analysis)
- (case members
- #;Nil
- #la;Unit
-
- (#;Cons singleton #;Nil)
- singleton
-
- (#;Cons left right)
- (#la;Product left (tuple right))))
-
(def: #export (analyse-product analyse membersC)
(-> &;Analyser (List Code) (Lux la;Analysis))
(do Monad<Lux>
@@ -143,13 +199,14 @@
(TC;read-var id))]
(&;with-expected-type expected'
(analyse-product analyse membersC)))
+ ## Must do inference...
(do @
[membersTA (mapM @ (|>. analyse &common;with-unknown-type)
membersC)
_ (&;within-type-env
(TC;check expected
(type;tuple (L/map product;left membersTA))))]
- (wrap (tuple (L/map product;right membersTA))))))
+ (wrap (product (L/map product;right membersTA))))))
(#;UnivQ _)
(do @
@@ -168,183 +225,91 @@
(&;fail "")
))))
-(def: (record-function-type type)
- (-> Type (Lux Type))
- (case type
- (#;Named name unnamedT)
- (do Monad<Lux>
- [unnamedT+ (record-function-type unnamedT)]
- (wrap (#;Named name unnamedT+)))
-
- (^template [<tag>]
- (<tag> env bodyT)
- (do Monad<Lux>
- [bodyT+ (record-function-type bodyT)]
- (wrap (<tag> env bodyT+))))
- ([#;UnivQ]
- [#;ExQ])
-
- (#;Product _)
- (:: Monad<Lux> wrap (type;function (type;flatten-tuple type) type))
-
- _
- (&;fail (format "Not a record type: " (%type type)))))
-
-(def: (out-of-bounds-error type size tag)
- (All [a] (-> Type Nat Nat (Lux a)))
- (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n"
- " Tag: " (%i (nat-to-int tag)) "\n"
- "Size: " (%i (nat-to-int size)) "\n"
- "Type: " (%type type))))
-
-(def: (variant-function-type tag expected-size type)
- (-> Nat Nat Type (Lux Type))
- (case type
- (#;Named name unnamedT)
- (do Monad<Lux>
- [unnamedT+ (variant-function-type tag expected-size unnamedT)]
- (wrap (#;Named name unnamedT+)))
-
- (^template [<tag>]
- (<tag> env bodyT)
- (do Monad<Lux>
- [bodyT+ (variant-function-type tag expected-size bodyT)]
- (wrap (<tag> env bodyT+))))
- ([#;UnivQ]
- [#;ExQ])
-
- (#;Sum _)
- (let [cases (type;flatten-variant type)
- actual-size (list;size cases)
- boundary (n.dec expected-size)]
- (cond (or (n.= expected-size actual-size)
- (and (n.> expected-size actual-size)
- (n.< boundary tag)))
- (case (list;nth tag cases)
- (#;Some caseT)
- (:: Monad<Lux> wrap (type;function (list caseT) type))
-
- #;None
- (out-of-bounds-error type expected-size tag))
-
- (n.< expected-size actual-size)
- (&;fail (format "Variant type is smaller than expected." "\n"
- "Expected: " (%i (nat-to-int expected-size)) "\n"
- " Actual: " (%i (nat-to-int actual-size))))
-
- (n.= boundary tag)
- (let [caseT (type;variant (list;drop boundary cases))]
- (:: Monad<Lux> wrap (type;function (list caseT) type)))
-
- ## else
- (out-of-bounds-error type expected-size tag)))
-
- _
- (&;fail (format "Not a variant type: " (%type type)))))
-
-(def: #export (analyse-record analyse members)
- (-> &;Analyser (List [Code Code]) (Lux la;Analysis))
- (do Monad<Lux>
- [members (normalize-record members)
- [members recordT] (order-record members)
- expectedT macro;expected-type
- functionT (record-function-type recordT)
- [inferredT membersA] (&inference;apply-function analyse functionT members)
- _ (&;within-type-env
- (TC;check expectedT inferredT))]
- (wrap (tuple membersA))))
-
-(do-template [<name> <side>]
- [(def: (<name> inner)
- (-> la;Analysis la;Analysis)
- (#la;Sum (<side> inner)))]
-
- [sum-left #;Left]
- [sum-right #;Right])
-
-(def: (variant tag size temp value)
- (-> Nat Nat Nat la;Analysis la;Analysis)
- (if (n.= (n.dec size) tag)
- (if (n.= +1 tag)
- (sum-right value)
- (L/fold (function;const sum-left)
- (sum-right value)
- (list;n.range +0 (n.- +2 tag))))
- (L/fold (function;const sum-left)
- (case value
- (#la;Sum _)
- (#la;Case value (list [(#la;BindP temp)
- (#la;Relative (#;Local temp))]))
-
- _
- value)
- (list;n.range +0 tag))))
-
(def: #export (analyse-tagged-sum analyse tag value)
(-> &;Analyser Ident Code (Lux la;Analysis))
(do Monad<Lux>
[tag (macro;normalize tag)
[idx group variantT] (macro;resolve-tag tag)
#let [case-size (list;size group)]
- functionT (variant-function-type idx case-size variantT)
- [inferredT valueA+] (&inference;apply-function analyse functionT (list value))
+ inferenceT (&inference;variant-inference-type idx case-size variantT)
+ [inferredT valueA+] (&inference;apply-function analyse inferenceT (list value))
expectedT macro;expected-type
_ (&;within-type-env
(TC;check expectedT inferredT))
temp &env;next-local]
(wrap (variant idx case-size temp (|> valueA+ list;head assume)))))
-(def: #export (analyse-sum analyse tag valueC)
- (-> &;Analyser Nat Code (Lux la;Analysis))
- (do Monad<Lux>
- [expected macro;expected-type]
- (&;with-stacked-errors
- (function [_] (format "Invalid type for variant: " (%type expected)))
- (case expected
- (#;Sum _)
- (let [flat (type;flatten-variant expected)
- type-size (list;size flat)]
- (case (list;nth tag flat)
- (#;Some variant-type)
- (do @
- [valueA (&;with-expected-type variant-type
- (analyse valueC))
- temp &env;next-local]
- (wrap (variant tag type-size temp valueA)))
+## 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]) (Lux (List [Ident Code])))
+ (mapM Monad<Lux>
+ (function [[key val]]
+ (case key
+ [_ (#;Tag key)]
+ (do Monad<Lux>
+ [key (macro;normalize key)]
+ (wrap [key val]))
- #;None
- (out-of-bounds-error expected type-size tag)))
+ _
+ (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key)))))
+ record))
- (#;Named name unnamedT)
- (&;with-expected-type unnamedT
- (analyse-sum analyse tag valueC))
+## 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]) (Lux [(List Code) Type]))
+ (case record
+ ## empty-record = empty-tuple = unit = []
+ #;Nil
+ (:: Monad<Lux> wrap [(list) Unit])
- (#;Var id)
- (do @
- [bound? (&;within-type-env
- (TC;bound? id))]
- (if bound?
- (do @
- [expected' (&;within-type-env
- (TC;read-var id))]
- (&;with-expected-type expected'
- (analyse-sum analyse tag valueC)))
- (&;fail (format "Invalid type for variant: " (%type expected)))))
+ (#;Cons [head-k head-v] _)
+ (do Monad<Lux>
+ [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 [])
+ (&;fail (format "Record size does not match tag-set size." "\n"
+ "Expected: " (|> size-ts nat-to-int %i) "\n"
+ " Actual: " (|> size-record nat-to-int %i) "\n"
+ "For type: " (%type recordT))))
+ #let [tuple-range (list;n.range +0 (n.dec size-ts))
+ tag->idx (D;from-list ident;Hash<Ident> (list;zip2 tag-set tuple-range))]
+ idx->val (foldM @
+ (function [[key val] idx->val]
+ (do @
+ [key (macro;normalize key)]
+ (case (D;get key tag->idx)
+ #;None
+ (&;fail (format "Tag " (%code (code;tag key))
+ " does not belong to tag-set for type " (%type recordT)))
- (#;UnivQ _)
- (do @
- [[var-id var] (&;within-type-env
- TC;existential)]
- (&;with-expected-type (assume (type;apply-type expected var))
- (analyse-sum analyse tag valueC)))
+ (#;Some idx)
+ (if (D;contains? idx idx->val)
+ (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key))))
+ (wrap (D;put idx val idx->val))))))
+ (: (D;Dict Nat Code)
+ (D;new number;Hash<Nat>))
+ record)
+ #let [ordered-tuple (L/map (function [idx] (assume (D;get idx idx->val)))
+ tuple-range)]]
+ (wrap [ordered-tuple recordT]))
+ ))
- (#;ExQ _)
- (&common;with-var
- (function [[var-id var]]
- (&;with-expected-type (assume (type;apply-type expected var))
- (analyse-sum analyse tag valueC))))
-
- _
- (if (n.= +0 tag)
- (analyse valueC)
- (&;fail ""))))))
+(def: #export (analyse-record analyse members)
+ (-> &;Analyser (List [Code Code]) (Lux la;Analysis))
+ (do Monad<Lux>
+ [members (normalize members)
+ [members recordT] (order members)
+ expectedT macro;expected-type
+ inferenceT (&inference;record-inference-type recordT)
+ [inferredT membersA] (&inference;apply-function analyse inferenceT members)
+ _ (&;within-type-env
+ (TC;check expectedT inferredT))]
+ (wrap (product membersA))))
diff --git a/new-luxc/source/luxc/analyser/type.lux b/new-luxc/source/luxc/analyser/type.lux
index 3b9b83245..1eb278d2a 100644
--- a/new-luxc/source/luxc/analyser/type.lux
+++ b/new-luxc/source/luxc/analyser/type.lux
@@ -6,7 +6,9 @@
(luxc ["&" base]
(lang ["la" analysis #+ Analysis])))
-## [Analysers]
+## These 2 analysers are somewhat special, since they require the
+## means of evaluating Lux expressions at compile-time for the sake of
+## computing Lux type values.
(def: #export (analyse-check analyse eval type value)
(-> &;Analyser &;Eval Code Code (Lux Analysis))
(do Monad<Lux>
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-27 09:49:49 +0000