aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib')
-rw-r--r--stdlib/source/lux/control/exception.lux22
-rw-r--r--stdlib/source/lux/data/coll/dictionary/plist.lux62
-rw-r--r--stdlib/source/lux/lang.lux3
-rw-r--r--stdlib/source/lux/lang/analysis.lux50
-rw-r--r--stdlib/source/lux/lang/analysis/expression.lux125
-rw-r--r--stdlib/source/lux/lang/analysis/inference.lux256
-rw-r--r--stdlib/source/lux/lang/analysis/structure.lux358
-rw-r--r--stdlib/source/lux/lang/module.lux239
-rw-r--r--stdlib/test/test/lux/lang/analysis/primitive.lux87
-rw-r--r--stdlib/test/test/lux/lang/analysis/structure.lux292
10 files changed, 1453 insertions, 41 deletions
diff --git a/stdlib/source/lux/control/exception.lux b/stdlib/source/lux/control/exception.lux
index b515f6c6b..d866c153e 100644
--- a/stdlib/source/lux/control/exception.lux
+++ b/stdlib/source/lux/control/exception.lux
@@ -4,8 +4,9 @@
["p" parser])
(data ["e" error]
[maybe]
+ [product]
[text "text/" Monoid<Text>]
- (coll [list "list/" Functor<List>]))
+ (coll [list "list/" Functor<List> Fold<List>]))
[macro]
(macro [code]
["s" syntax #+ syntax: Syntax]
@@ -99,3 +100,22 @@
((~! text/compose) (~ g!descriptor)
(~ (maybe.default (' "") body))))})))))
)))
+
+(def: #export (report' entries)
+ (-> (List [Text Text]) Text)
+ (let [largest-header-size (|> entries
+ (list/map (|>> product.left text.size))
+ (list/fold n/max +0))]
+ (|> entries
+ (list/map (function (_ [header message])
+ (let [padding (|> " "
+ (list.repeat (n/- (text.size header)
+ largest-header-size))
+ (text.join-with ""))]
+ ($_ text/compose padding header ": " message))))
+ (text.join-with "\n"))))
+
+(syntax: #export (report {entries (p.many (s.tuple (p.seq s.any s.any)))})
+ (wrap (list (` (report' (list (~+ (|> entries
+ (list/map (function (_ [header message])
+ (` [(~ header) (~ message)])))))))))))
diff --git a/stdlib/source/lux/data/coll/dictionary/plist.lux b/stdlib/source/lux/data/coll/dictionary/plist.lux
new file mode 100644
index 000000000..e9e08107a
--- /dev/null
+++ b/stdlib/source/lux/data/coll/dictionary/plist.lux
@@ -0,0 +1,62 @@
+(.module:
+ lux
+ (lux (data [text "text/" Eq<Text>])))
+
+(type: #export (PList a)
+ (List [Text a]))
+
+(def: #export (get key properties)
+ (All [a] (-> Text (PList a) (Maybe a)))
+ (case properties
+ #.Nil
+ #.None
+
+ (#.Cons [k' v'] properties')
+ (if (text/= key k')
+ (#.Some v')
+ (get key properties'))))
+
+(def: #export (contains? key properties)
+ (All [a] (-> Text (PList a) Bool))
+ (case (get key properties)
+ (#.Some _)
+ true
+
+ #.None
+ false))
+
+(def: #export (put key val properties)
+ (All [a] (-> Text a (PList a) (PList a)))
+ (case properties
+ #.Nil
+ (list [key val])
+
+ (#.Cons [k' v'] properties')
+ (if (text/= key k')
+ (#.Cons [key val]
+ properties')
+ (#.Cons [k' v']
+ (put key val properties')))))
+
+(def: #export (update key f properties)
+ (All [a] (-> Text (-> a a) (PList a) (PList a)))
+ (case properties
+ #.Nil
+ #.Nil
+
+ (#.Cons [k' v'] properties')
+ (if (text/= key k')
+ (#.Cons [k' (f v')] properties')
+ (#.Cons [k' v'] (update key f properties')))))
+
+(def: #export (remove key properties)
+ (All [a] (-> Text (PList a) (PList a)))
+ (case properties
+ #.Nil
+ properties
+
+ (#.Cons [k' v'] properties')
+ (if (text/= key k')
+ properties'
+ (#.Cons [k' v']
+ (remove key properties')))))
diff --git a/stdlib/source/lux/lang.lux b/stdlib/source/lux/lang.lux
index c4a4e2db3..9f164b719 100644
--- a/stdlib/source/lux/lang.lux
+++ b/stdlib/source/lux/lang.lux
@@ -9,6 +9,9 @@
[macro]
(macro ["s" syntax #+ syntax:])))
+(type: #export Eval
+ (-> Type Code (Meta Top)))
+
(def: #export (fail message)
(All [a] (-> Text (Meta a)))
(do macro.Monad<Meta>
diff --git a/stdlib/source/lux/lang/analysis.lux b/stdlib/source/lux/lang/analysis.lux
index 46927bae1..6b2ba097d 100644
--- a/stdlib/source/lux/lang/analysis.lux
+++ b/stdlib/source/lux/lang/analysis.lux
@@ -48,10 +48,12 @@
(#Constant Ident)
(#Special (Special Text)))
-## 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.
+(type: #export Variant
+ {#lefts Nat
+ #right? Bool
+ #value Analysis})
+
+(type: #export Tuple (List Analysis))
(do-template [<name> <tag>]
[(def: <name>
@@ -71,8 +73,8 @@
(let [identity (#Function (list) (#Variable (#Local +1)))]
(#Apply value identity)))
-(def: #export (sum tag size temp value)
- (-> Tag Nat Register Analysis Analysis)
+(def: #export (sum size tag value)
+ (-> Nat Tag Analysis Analysis)
(if (last? size tag)
(if (n/= +1 tag)
(..right value)
@@ -88,8 +90,8 @@
value)
(list.n/range +0 tag))))
-(def: #export (tuple members)
- (-> (List Analysis) Analysis)
+(def: #export (product members)
+ (-> Tuple Analysis)
(case (list.reverse members)
#.Nil
(#Primitive #Unit)
@@ -107,3 +109,35 @@
(type: #export Analyser
(-> Code (Meta Analysis)))
+
+(def: #export (tuple analysis)
+ (-> Analysis Tuple)
+ (case analysis
+ (#Structure (#Product left right))
+ (#.Cons left (tuple right))
+
+ _
+ (list analysis)))
+
+(def: #export (variant analysis)
+ (-> Analysis (Maybe Variant))
+ (loop [lefts +0
+ variantA analysis]
+ (case variantA
+ (#Structure (#Sum (#.Left valueA)))
+ (case valueA
+ (#Structure (#Sum _))
+ (recur (inc lefts) valueA)
+
+ _
+ (#.Some {#lefts lefts
+ #right? false
+ #value valueA}))
+
+ (#Structure (#Sum (#.Right valueA)))
+ (#.Some {#lefts lefts
+ #right? true
+ #value valueA})
+
+ _
+ #.None)))
diff --git a/stdlib/source/lux/lang/analysis/expression.lux b/stdlib/source/lux/lang/analysis/expression.lux
new file mode 100644
index 000000000..a22e3d32b
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/expression.lux
@@ -0,0 +1,125 @@
+(.module:
+ lux
+ (lux (control [monad #+ do]
+ ["ex" exception #+ exception:])
+ (data ["e" error]
+ [product]
+ text/format)
+ [macro]
+ [lang #+ Eval]
+ (lang [type]
+ (type ["tc" check])
+ [".L" analysis #+ Analysis Analyser]
+ (analysis [".A" type]
+ [".A" primitive]
+ [".A" structure]
+ ## [".A" function]
+ ## [".A" reference]
+ )
+ ## [".L" macro]
+ ## [".L" extension]
+ )))
+
+(exception: #export (macro-expansion-failed {message Text})
+ message)
+
+(do-template [<name>]
+ [(exception: #export (<name> {code Code})
+ (%code code))]
+
+ [macro-call-must-have-single-expansion]
+ [unrecognized-syntax]
+ )
+
+(def: #export (analyser eval)
+ (-> Eval Analyser)
+ (: (-> Code (Meta Analysis))
+ (function (analyse code)
+ (do macro.Monad<Meta>
+ [expectedT macro.expected-type]
+ (let [[cursor code'] code]
+ ## The cursor must be set in the compiler for the sake
+ ## of having useful error messages.
+ (lang.with-cursor cursor
+ (case code'
+ (^template [<tag> <analyser>]
+ (<tag> value)
+ (<analyser> value))
+ ([#.Bool primitiveA.bool]
+ [#.Nat primitiveA.nat]
+ [#.Int primitiveA.int]
+ [#.Deg primitiveA.deg]
+ [#.Frac primitiveA.frac]
+ [#.Text primitiveA.text])
+
+ (^template [<tag> <analyser>]
+ (^ (#.Form (list& [_ (<tag> tag)]
+ values)))
+ (case values
+ (#.Cons value #.Nil)
+ (<analyser> analyse tag value)
+
+ _
+ (<analyser> analyse tag (` [(~+ values)]))))
+ ([#.Nat structureA.sum]
+ [#.Tag structureA.tagged-sum])
+
+ (#.Tag tag)
+ (structureA.tagged-sum analyse tag (' []))
+
+ (^ (#.Tuple (list)))
+ primitiveA.unit
+
+ (^ (#.Tuple (list singleton)))
+ (analyse singleton)
+
+ (^ (#.Tuple elems))
+ (structureA.product analyse elems)
+
+ (^ (#.Record pairs))
+ (structureA.record analyse pairs)
+
+ ## (#.Symbol reference)
+ ## (referenceA.analyse-reference reference)
+
+ ## (^ (#.Form (list& [_ (#.Text proc-name)] proc-args)))
+ ## (do macro.Monad<Meta>
+ ## [procedure (extensionL.find-analysis proc-name)]
+ ## (procedure analyse eval proc-args))
+
+ ## (^ (#.Form (list& func args)))
+ ## (do macro.Monad<Meta>
+ ## [[funcT funcA] (typeA.with-inference
+ ## (analyse func))]
+ ## (case funcA
+ ## [_ (#.Symbol def-name)]
+ ## (do @
+ ## [?macro (lang.with-error-tracking
+ ## (macro.find-macro def-name))]
+ ## (case ?macro
+ ## (#.Some macro)
+ ## (do @
+ ## [expansion (: (Meta (List Code))
+ ## (function (_ compiler)
+ ## (case (macroL.expand macro args compiler)
+ ## (#e.Error error)
+ ## ((lang.throw macro-expansion-failed error) compiler)
+
+ ## output
+ ## output)))]
+ ## (case expansion
+ ## (^ (list single))
+ ## (analyse single)
+
+ ## _
+ ## (lang.throw macro-call-must-have-single-expansion code)))
+
+ ## _
+ ## (functionA.analyse-apply analyse funcT funcA args)))
+
+ ## _
+ ## (functionA.analyse-apply analyse funcT funcA args)))
+
+ _
+ (lang.throw unrecognized-syntax code)
+ )))))))
diff --git a/stdlib/source/lux/lang/analysis/inference.lux b/stdlib/source/lux/lang/analysis/inference.lux
new file mode 100644
index 000000000..732a8e6e3
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/inference.lux
@@ -0,0 +1,256 @@
+(.module:
+ lux
+ (lux (control [monad #+ do]
+ ["ex" exception #+ exception:])
+ (data [maybe]
+ [text]
+ text/format
+ (coll [list "list/" Functor<List>]))
+ [macro "macro/" Monad<Meta>]
+ [lang]
+ (lang [type]
+ (type ["tc" check])
+ [analysis #+ Analysis Analyser]
+ (analysis [".A" type]))))
+
+(exception: #export (variant-tag-out-of-bounds {size Nat} {tag analysis.Tag} {type Type})
+ (ex.report ["Tag" (%n tag)]
+ ["Variant size" (%n size)]
+ ["Variant type" (%type type)]))
+
+(exception: #export (cannot-infer {type Type} {args (List Code)})
+ (ex.report ["Type" (%type type)]
+ ["Arguments" (|> args
+ list.enumerate
+ (list/map (function (_ [idx argC])
+ (format "\n " (%n idx) " " (%code argC))))
+ (text.join-with ""))]))
+
+(exception: #export (cannot-infer-argument {inferred Type} {argument Code})
+ (ex.report ["Inferred Type" (%type inferred)]
+ ["Argument" (%code argument)]))
+
+(exception: #export (smaller-variant-than-expected {expected Nat} {actual Nat})
+ (ex.report ["Expected" (%i (.int expected))]
+ ["Actual" (%i (.int actual))]))
+
+(do-template [<name>]
+ [(exception: #export (<name> {type Type})
+ (%type type))]
+
+ [not-a-variant-type]
+ [not-a-record-type]
+ [invalid-type-application]
+ )
+
+(def: (replace-bound bound-idx replacementT type)
+ (-> Nat Type Type Type)
+ (case type
+ (#.Primitive name params)
+ (#.Primitive name (list/map (replace-bound bound-idx replacementT) params))
+
+ (^template [<tag>]
+ (<tag> left right)
+ (<tag> (replace-bound bound-idx replacementT left)
+ (replace-bound bound-idx replacementT right)))
+ ([#.Sum]
+ [#.Product]
+ [#.Function]
+ [#.Apply])
+
+ (#.Bound idx)
+ (if (n/= bound-idx idx)
+ replacementT
+ type)
+
+ (^template [<tag>]
+ (<tag> env quantified)
+ (<tag> (list/map (replace-bound bound-idx replacementT) env)
+ (replace-bound (n/+ +2 bound-idx) replacementT quantified)))
+ ([#.UnivQ]
+ [#.ExQ])
+
+ _
+ type))
+
+(def: new-named-type
+ (Meta Type)
+ (do macro.Monad<Meta>
+ [[_module _line _column] macro.cursor
+ [ex-id exT] (typeA.with-env tc.existential)]
+ (wrap (#.Primitive (format "{New Type @ " (%t _module)
+ "," (%n _line)
+ "," (%n _column)
+ "} " (%n ex-id))
+ (list)))))
+
+## 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 treated
+## as a function type, this method of inference should work.
+(def: #export (general analyse inferT args)
+ (-> Analyser Type (List Code) (Meta [Type (List Analysis)]))
+ (case args
+ #.Nil
+ (do macro.Monad<Meta>
+ [_ (typeA.infer inferT)]
+ (wrap [inferT (list)]))
+
+ (#.Cons argC args')
+ (case inferT
+ (#.Named name unnamedT)
+ (general analyse unnamedT args)
+
+ (#.UnivQ _)
+ (do macro.Monad<Meta>
+ [[var-id varT] (typeA.with-env tc.var)]
+ (general analyse (maybe.assume (type.apply (list varT) inferT)) args))
+
+ (#.ExQ _)
+ (do macro.Monad<Meta>
+ [[var-id varT] (typeA.with-env tc.var)
+ output (general analyse
+ (maybe.assume (type.apply (list varT) inferT))
+ args)
+ bound? (typeA.with-env
+ (tc.bound? var-id))
+ _ (if bound?
+ (wrap [])
+ (do @
+ [newT new-named-type]
+ (typeA.with-env
+ (tc.check varT newT))))]
+ (wrap output))
+
+ (#.Apply inputT transT)
+ (case (type.apply (list inputT) transT)
+ (#.Some outputT)
+ (general analyse outputT args)
+
+ #.None
+ (lang.throw invalid-type-application inferT))
+
+ ## 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 macro.Monad<Meta>
+ [[outputT' args'A] (general analyse outputT args')
+ argA (lang.with-stacked-errors
+ (function (_ _)
+ (ex.construct cannot-infer-argument [inputT argC]))
+ (typeA.with-type inputT
+ (analyse argC)))]
+ (wrap [outputT' (list& argA args'A)]))
+
+ (#.Var infer-id)
+ (do macro.Monad<Meta>
+ [?inferT' (typeA.with-env (tc.read infer-id))]
+ (case ?inferT'
+ (#.Some inferT')
+ (general analyse inferT' args)
+
+ _
+ (lang.throw cannot-infer [inferT args])))
+
+ _
+ (lang.throw cannot-infer [inferT args]))
+ ))
+
+## Turns a record type into the kind of function type suitable for inference.
+(def: #export (record inferT)
+ (-> Type (Meta Type))
+ (case inferT
+ (#.Named name unnamedT)
+ (record unnamedT)
+
+ (^template [<tag>]
+ (<tag> env bodyT)
+ (do macro.Monad<Meta>
+ [bodyT+ (record bodyT)]
+ (wrap (<tag> env bodyT+))))
+ ([#.UnivQ]
+ [#.ExQ])
+
+ (#.Apply inputT funcT)
+ (case (type.apply (list inputT) funcT)
+ (#.Some outputT)
+ (record outputT)
+
+ #.None
+ (lang.throw invalid-type-application inferT))
+
+ (#.Product _)
+ (macro/wrap (type.function (type.flatten-tuple inferT) inferT))
+
+ _
+ (lang.throw not-a-record-type inferT)))
+
+## Turns a variant type into the kind of function type suitable for inference.
+(def: #export (variant tag expected-size inferT)
+ (-> Nat Nat Type (Meta Type))
+ (loop [depth +0
+ currentT inferT]
+ (case currentT
+ (#.Named name unnamedT)
+ (do macro.Monad<Meta>
+ [unnamedT+ (recur depth unnamedT)]
+ (wrap unnamedT+))
+
+ (^template [<tag>]
+ (<tag> env bodyT)
+ (do macro.Monad<Meta>
+ [bodyT+ (recur (inc depth) bodyT)]
+ (wrap (<tag> env bodyT+))))
+ ([#.UnivQ]
+ [#.ExQ])
+
+ (#.Sum _)
+ (let [cases (type.flatten-variant currentT)
+ actual-size (list.size cases)
+ boundary (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)
+ (macro/wrap (if (n/= +0 depth)
+ (type.function (list caseT) currentT)
+ (let [replace! (replace-bound (|> depth dec (n/* +2)) inferT)]
+ (type.function (list (replace! caseT))
+ (replace! currentT)))))
+
+ #.None
+ (lang.throw variant-tag-out-of-bounds [expected-size tag inferT]))
+
+ (n/< expected-size actual-size)
+ (lang.throw smaller-variant-than-expected [expected-size actual-size])
+
+ (n/= boundary tag)
+ (let [caseT (type.variant (list.drop boundary cases))]
+ (macro/wrap (if (n/= +0 depth)
+ (type.function (list caseT) currentT)
+ (let [replace! (replace-bound (|> depth dec (n/* +2)) inferT)]
+ (type.function (list (replace! caseT))
+ (replace! currentT))))))
+
+ ## else
+ (lang.throw variant-tag-out-of-bounds [expected-size tag inferT])))
+
+ (#.Apply inputT funcT)
+ (case (type.apply (list inputT) funcT)
+ (#.Some outputT)
+ (variant tag expected-size outputT)
+
+ #.None
+ (lang.throw invalid-type-application inferT))
+
+ _
+ (lang.throw not-a-variant-type inferT))))
diff --git a/stdlib/source/lux/lang/analysis/structure.lux b/stdlib/source/lux/lang/analysis/structure.lux
new file mode 100644
index 000000000..cc185ebe9
--- /dev/null
+++ b/stdlib/source/lux/lang/analysis/structure.lux
@@ -0,0 +1,358 @@
+(.module:
+ lux
+ (lux (control [monad #+ do]
+ ["ex" exception #+ exception:])
+ (data [ident]
+ [number]
+ [product]
+ [maybe]
+ (coll [list "list/" Functor<List>]
+ (dictionary ["dict" unordered #+ Dict]))
+ text/format)
+ [macro]
+ (macro [code])
+ [lang]
+ (lang [type]
+ (type ["tc" check])
+ [analysis #+ Analysis Analyser]
+ (analysis [".A" type]
+ [".A" primitive]
+ [".A" inference]))))
+
+(exception: #export (invalid-variant-type {type Type} {tag analysis.Tag} {code Code})
+ (ex.report ["Type" (%type type)]
+ ["Tag" (%n tag)]
+ ["Expression" (%code code)]))
+
+(do-template [<name>]
+ [(exception: #export (<name> {type Type} {members (List Code)})
+ (ex.report ["Type" (%type type)]
+ ["Expression" (%code (` [(~+ members)]))]))]
+
+ [invalid-tuple-type]
+ [cannot-analyse-tuple]
+ )
+
+(exception: #export (not-a-quantified-type {type Type})
+ (%type type))
+
+(do-template [<name>]
+ [(exception: #export (<name> {type Type} {tag analysis.Tag} {code Code})
+ (ex.report ["Type" (%type type)]
+ ["Tag" (%n tag)]
+ ["Expression" (%code code)]))]
+
+ [cannot-analyse-variant]
+ [cannot-infer-numeric-tag]
+ )
+
+(exception: #export (record-keys-must-be-tags {key Code} {record (List [Code Code])})
+ (ex.report ["Key" (%code key)]
+ ["Record" (%code (code.record record))]))
+
+(do-template [<name>]
+ [(exception: #export (<name> {key Ident} {record (List [Ident Code])})
+ (ex.report ["Tag" (%code (code.tag key))]
+ ["Record" (%code (code.record (list/map (function (_ [keyI valC])
+ [(code.tag keyI) valC])
+ record)))]))]
+
+ [cannot-repeat-tag]
+ )
+
+(exception: #export (tag-does-not-belong-to-record {key Ident} {type Type})
+ (ex.report ["Tag" (%code (code.tag key))]
+ ["Type" (%type type)]))
+
+(exception: #export (record-size-mismatch {expected Nat} {actual Nat} {type Type} {record (List [Ident Code])})
+ (ex.report ["Expected" (|> expected .int %i)]
+ ["Actual" (|> actual .int %i)]
+ ["Type" (%type type)]
+ ["Expression" (%code (|> record
+ (list/map (function (_ [keyI valueC])
+ [(code.tag keyI) valueC]))
+ code.record))]))
+
+(def: #export (sum analyse tag valueC)
+ (-> Analyser Nat Code (Meta Analysis))
+ (do macro.Monad<Meta>
+ [expectedT macro.expected-type]
+ (lang.with-stacked-errors
+ (function (_ _)
+ (ex.construct cannot-analyse-variant [expectedT tag 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 (typeA.with-type variant-type
+ (analyse valueC))]
+ (wrap (analysis.sum type-size tag valueA)))
+
+ #.None
+ (lang.throw inferenceA.variant-tag-out-of-bounds [type-size tag expectedT])))
+
+ (#.Named name unnamedT)
+ (typeA.with-type unnamedT
+ (sum analyse tag valueC))
+
+ (#.Var id)
+ (do @
+ [?expectedT' (typeA.with-env
+ (tc.read id))]
+ (case ?expectedT'
+ (#.Some expectedT')
+ (typeA.with-type expectedT'
+ (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.
+ (lang.throw cannot-infer-numeric-tag [expectedT tag valueC])
+ ))
+
+ (^template [<tag> <instancer>]
+ (<tag> _)
+ (do @
+ [[instance-id instanceT] (typeA.with-env <instancer>)]
+ (typeA.with-type (maybe.assume (type.apply (list instanceT) expectedT))
+ (sum analyse tag valueC))))
+ ([#.UnivQ tc.existential]
+ [#.ExQ tc.var])
+
+ (#.Apply inputT funT)
+ (case funT
+ (#.Var funT-id)
+ (do @
+ [?funT' (typeA.with-env (tc.read funT-id))]
+ (case ?funT'
+ (#.Some funT')
+ (typeA.with-type (#.Apply inputT funT')
+ (sum analyse tag valueC))
+
+ _
+ (lang.throw invalid-variant-type [expectedT tag valueC])))
+
+ _
+ (case (type.apply (list inputT) funT)
+ #.None
+ (lang.throw not-a-quantified-type funT)
+
+ (#.Some outputT)
+ (typeA.with-type outputT
+ (sum analyse tag valueC))))
+
+ _
+ (lang.throw invalid-variant-type [expectedT tag valueC])))))
+
+(def: (typed-product analyse membersC+)
+ (-> Analyser (List Code) (Meta Analysis))
+ (do macro.Monad<Meta>
+ [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)]
+ (typeA.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 (typeA.with-type leftT
+ (analyse leftC))
+ rightA (recur rightT rightC)]
+ (wrap (#analysis.Structure (#analysis.Product leftA rightA))))
+
+ ## If, however, the type runs out but there is still enough
+ ## tail, the remaining elements get packaged into another
+ ## tuple.
+ ## 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.
+ [tailT tailC]
+ (|> tailC
+ code.tuple
+ analyse
+ (typeA.with-type tailT)
+ (:: @ map analysis.no-op))))))
+
+(def: #export (product analyse membersC)
+ (-> Analyser (List Code) (Meta Analysis))
+ (do macro.Monad<Meta>
+ [expectedT macro.expected-type]
+ (lang.with-stacked-errors
+ (function (_ _)
+ (ex.construct cannot-analyse-tuple [expectedT membersC]))
+ (case expectedT
+ (#.Product _)
+ (..typed-product analyse membersC)
+
+ (#.Named name unnamedT)
+ (typeA.with-type unnamedT
+ (product analyse membersC))
+
+ (#.Var id)
+ (do @
+ [?expectedT' (typeA.with-env
+ (tc.read id))]
+ (case ?expectedT'
+ (#.Some expectedT')
+ (typeA.with-type expectedT'
+ (product analyse membersC))
+
+ _
+ ## Must do inference...
+ (do @
+ [membersTA (monad.map @ (|>> analyse typeA.with-inference)
+ membersC)
+ _ (typeA.with-env
+ (tc.check expectedT
+ (type.tuple (list/map product.left membersTA))))]
+ (wrap (analysis.product (list/map product.right membersTA))))))
+
+ (^template [<tag> <instancer>]
+ (<tag> _)
+ (do @
+ [[instance-id instanceT] (typeA.with-env <instancer>)]
+ (typeA.with-type (maybe.assume (type.apply (list instanceT) expectedT))
+ (product analyse membersC))))
+ ([#.UnivQ tc.existential]
+ [#.ExQ tc.var])
+
+ (#.Apply inputT funT)
+ (case funT
+ (#.Var funT-id)
+ (do @
+ [?funT' (typeA.with-env (tc.read funT-id))]
+ (case ?funT'
+ (#.Some funT')
+ (typeA.with-type (#.Apply inputT funT')
+ (product analyse membersC))
+
+ _
+ (lang.throw invalid-tuple-type [expectedT membersC])))
+
+ _
+ (case (type.apply (list inputT) funT)
+ #.None
+ (lang.throw not-a-quantified-type funT)
+
+ (#.Some outputT)
+ (typeA.with-type outputT
+ (product analyse membersC))))
+
+ _
+ (lang.throw invalid-tuple-type [expectedT membersC])
+ ))))
+
+(def: #export (tagged-sum analyse tag valueC)
+ (-> Analyser Ident Code (Meta Analysis))
+ (do macro.Monad<Meta>
+ [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 (inferenceA.variant idx case-size variantT)
+ [inferredT valueA+] (inferenceA.general analyse inferenceT (list valueC))]
+ (wrap (analysis.sum case-size idx (|> valueA+ list.head maybe.assume))))
+
+ _
+ (..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<Meta>
+ (function (_ [key val])
+ (case key
+ [_ (#.Tag key)]
+ (do macro.Monad<Meta>
+ [key (macro.normalize key)]
+ (wrap [key val]))
+
+ _
+ (lang.throw record-keys-must-be-tags [key 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<Meta> wrap [(list) Top])
+
+ (#.Cons [head-k head-v] _)
+ (do macro.Monad<Meta>
+ [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 [])
+ (lang.throw record-size-mismatch [size-ts size-record recordT record]))
+ #let [tuple-range (list.n/range +0 (dec size-ts))
+ tag->idx (dict.from-list ident.Hash<Ident> (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
+ (lang.throw tag-does-not-belong-to-record [key recordT])
+
+ (#.Some idx)
+ (if (dict.contains? idx idx->val)
+ (lang.throw cannot-repeat-tag [key record])
+ (wrap (dict.put idx val idx->val))))))
+ (: (Dict Nat Code)
+ (dict.new number.Hash<Nat>))
+ record)
+ #let [ordered-tuple (list/map (function (_ idx) (maybe.assume (dict.get idx idx->val)))
+ tuple-range)]]
+ (wrap [ordered-tuple recordT]))
+ ))
+
+(def: #export (record analyse members)
+ (-> Analyser (List [Code Code]) (Meta Analysis))
+ (do macro.Monad<Meta>
+ [members (normalize members)
+ [membersC recordT] (order members)]
+ (case membersC
+ (^ (list))
+ primitiveA.unit
+
+ (^ (list singletonC))
+ (analyse singletonC)
+
+ _
+ (do @
+ [expectedT macro.expected-type]
+ (case expectedT
+ (#.Var _)
+ (do @
+ [inferenceT (inferenceA.record recordT)
+ [inferredT membersA] (inferenceA.general analyse inferenceT membersC)]
+ (wrap (analysis.product membersA)))
+
+ _
+ (..product analyse membersC))))))
diff --git a/stdlib/source/lux/lang/module.lux b/stdlib/source/lux/lang/module.lux
new file mode 100644
index 000000000..d5efb1d7e
--- /dev/null
+++ b/stdlib/source/lux/lang/module.lux
@@ -0,0 +1,239 @@
+(.module:
+ lux
+ (lux (control [monad #+ do]
+ ["ex" exception #+ exception:]
+ pipe)
+ (data [text "text/" Eq<Text>]
+ text/format
+ ["e" error]
+ (coll [list "list/" Fold<List> Functor<List>]
+ (dictionary [plist])))
+ [macro])
+ [//])
+
+(type: #export Tag Text)
+
+(exception: #export (unknown-module {module Text})
+ module)
+
+(exception: #export (cannot-declare-tag-twice {module Text} {tag Text})
+ (format "Module: " module "\n"
+ " Tag: " tag "\n"))
+
+(do-template [<name>]
+ [(exception: #export (<name> {tags (List Text)} {owner Type})
+ (format "Tags: " (text.join-with " " tags) "\n"
+ "Type: " (%type owner) "\n"))]
+
+ [cannot-declare-tags-for-unnamed-type]
+ [cannot-declare-tags-for-foreign-type]
+ )
+
+(exception: #export (cannot-define-more-than-once {name Ident})
+ (%ident name))
+
+(exception: #export (can-only-change-state-of-active-module {module Text} {state Module-State})
+ (format " Module: " module "\n"
+ "Desired state: " (case state
+ #.Active "Active"
+ #.Compiled "Compiled"
+ #.Cached "Cached") "\n"))
+
+(exception: #export (cannot-set-module-annotations-more-than-once {module Text} {old Code} {new Code})
+ (format " Module: " module "\n"
+ "Old annotations: " (%code old) "\n"
+ "New annotations: " (%code new) "\n"))
+
+(def: (new hash)
+ (-> Nat Module)
+ {#.module-hash hash
+ #.module-aliases (list)
+ #.definitions (list)
+ #.imports (list)
+ #.tags (list)
+ #.types (list)
+ #.module-annotations #.None
+ #.module-state #.Active})
+
+(def: #export (set-annotations annotations)
+ (-> Code (Meta Top))
+ (do macro.Monad<Meta>
+ [self-name macro.current-module-name
+ self macro.current-module]
+ (case (get@ #.module-annotations self)
+ #.None
+ (function (_ compiler)
+ (#e.Success [(update@ #.modules
+ (plist.put self-name (set@ #.module-annotations (#.Some annotations) self))
+ compiler)
+ []]))
+
+ (#.Some old)
+ (//.throw cannot-set-module-annotations-more-than-once [self-name old annotations]))))
+
+(def: #export (import module)
+ (-> Text (Meta Top))
+ (do macro.Monad<Meta>
+ [self-name macro.current-module-name]
+ (function (_ compiler)
+ (#e.Success [(update@ #.modules
+ (plist.update self-name (update@ #.imports (|>> (#.Cons module))))
+ compiler)
+ []]))))
+
+(def: #export (alias alias module)
+ (-> Text Text (Meta Top))
+ (do macro.Monad<Meta>
+ [self-name macro.current-module-name]
+ (function (_ compiler)
+ (#e.Success [(update@ #.modules
+ (plist.update self-name (update@ #.module-aliases (: (-> (List [Text Text]) (List [Text Text]))
+ (|>> (#.Cons [alias module])))))
+ compiler)
+ []]))))
+
+(def: #export (exists? module)
+ (-> Text (Meta Bool))
+ (function (_ compiler)
+ (|> compiler
+ (get@ #.modules)
+ (plist.get module)
+ (case> (#.Some _) true #.None false)
+ [compiler] #e.Success)))
+
+(def: #export (define name definition)
+ (-> Text Definition (Meta []))
+ (do macro.Monad<Meta>
+ [self-name macro.current-module-name
+ self macro.current-module]
+ (function (_ compiler)
+ (case (plist.get name (get@ #.definitions self))
+ #.None
+ (#e.Success [(update@ #.modules
+ (plist.put self-name
+ (update@ #.definitions
+ (: (-> (List [Text Definition]) (List [Text Definition]))
+ (|>> (#.Cons [name definition])))
+ self))
+ compiler)
+ []])
+
+ (#.Some already-existing)
+ ((//.throw cannot-define-more-than-once [self-name name]) compiler)))))
+
+(def: #export (create hash name)
+ (-> Nat Text (Meta []))
+ (function (_ compiler)
+ (let [module (new hash)]
+ (#e.Success [(update@ #.modules
+ (plist.put name module)
+ compiler)
+ []]))))
+
+(def: #export (with-module hash name action)
+ (All [a] (-> Nat Text (Meta a) (Meta [Module a])))
+ (do macro.Monad<Meta>
+ [_ (create hash name)
+ output (//.with-current-module name
+ action)
+ module (macro.find-module name)]
+ (wrap [module output])))
+
+(do-template [<setter> <asker> <tag>]
+ [(def: #export (<setter> module-name)
+ (-> Text (Meta Top))
+ (function (_ compiler)
+ (case (|> compiler (get@ #.modules) (plist.get module-name))
+ (#.Some module)
+ (let [active? (case (get@ #.module-state module)
+ #.Active true
+ _ false)]
+ (if active?
+ (#e.Success [(update@ #.modules
+ (plist.put module-name (set@ #.module-state <tag> module))
+ compiler)
+ []])
+ ((//.throw can-only-change-state-of-active-module [module-name <tag>])
+ compiler)))
+
+ #.None
+ ((//.throw unknown-module module-name) compiler))))
+
+ (def: #export (<asker> module-name)
+ (-> Text (Meta Bool))
+ (function (_ compiler)
+ (case (|> compiler (get@ #.modules) (plist.get module-name))
+ (#.Some module)
+ (#e.Success [compiler
+ (case (get@ #.module-state module)
+ <tag> true
+ _ false)])
+
+ #.None
+ ((//.throw unknown-module module-name) compiler))))]
+
+ [set-active active? #.Active]
+ [set-compiled compiled? #.Compiled]
+ [set-cached cached? #.Cached]
+ )
+
+(do-template [<name> <tag> <type>]
+ [(def: (<name> module-name)
+ (-> Text (Meta <type>))
+ (function (_ compiler)
+ (case (|> compiler (get@ #.modules) (plist.get module-name))
+ (#.Some module)
+ (#e.Success [compiler (get@ <tag> module)])
+
+ #.None
+ ((//.throw unknown-module module-name) compiler))))]
+
+ [tags #.tags (List [Text [Nat (List Ident) Bool Type]])]
+ [types #.types (List [Text [(List Ident) Bool Type]])]
+ [hash #.module-hash Nat]
+ )
+
+(def: (ensure-undeclared-tags module-name tags)
+ (-> Text (List Tag) (Meta Top))
+ (do macro.Monad<Meta>
+ [bindings (..tags module-name)
+ _ (monad.map @
+ (function (_ tag)
+ (case (plist.get tag bindings)
+ #.None
+ (wrap [])
+
+ (#.Some _)
+ (//.throw cannot-declare-tag-twice [module-name tag])))
+ tags)]
+ (wrap [])))
+
+(def: #export (declare-tags tags exported? type)
+ (-> (List Tag) Bool Type (Meta Top))
+ (do macro.Monad<Meta>
+ [self-name macro.current-module-name
+ [type-module type-name] (case type
+ (#.Named type-ident _)
+ (wrap type-ident)
+
+ _
+ (//.throw cannot-declare-tags-for-unnamed-type [tags type]))
+ _ (ensure-undeclared-tags self-name tags)
+ _ (//.assert cannot-declare-tags-for-foreign-type [tags type]
+ (text/= self-name type-module))]
+ (function (_ compiler)
+ (case (|> compiler (get@ #.modules) (plist.get self-name))
+ (#.Some module)
+ (let [namespaced-tags (list/map (|>> [self-name]) tags)]
+ (#e.Success [(update@ #.modules
+ (plist.update self-name
+ (|>> (update@ #.tags (function (_ tag-bindings)
+ (list/fold (function (_ [idx tag] table)
+ (plist.put tag [idx namespaced-tags exported? type] table))
+ tag-bindings
+ (list.enumerate tags))))
+ (update@ #.types (plist.put type-name [namespaced-tags exported? type]))))
+ compiler)
+ []]))
+ #.None
+ ((//.throw unknown-module self-name) compiler)))))
diff --git a/stdlib/test/test/lux/lang/analysis/primitive.lux b/stdlib/test/test/lux/lang/analysis/primitive.lux
index 2e7c2057a..ed9d8bfc6 100644
--- a/stdlib/test/test/lux/lang/analysis/primitive.lux
+++ b/stdlib/test/test/lux/lang/analysis/primitive.lux
@@ -1,24 +1,46 @@
(.module:
- lux
+ [lux #- primitive]
(lux [io]
(control [monad #+ do]
pipe
["ex" exception #+ exception:])
(data (text format)
["e" error])
- ["r" math/random]
+ ["r" math/random "r/" Monad<Random>]
[macro]
(macro [code])
+ [lang]
(lang [".L" type "type/" Eq<Type>]
[".L" init]
[analysis #+ Analysis]
(analysis [".A" type]
- ["/" primitive]))
+ [".A" expression]))
test))
+(def: analyse (expressionA.analyser (:! lang.Eval [])))
+
+(def: unit
+ (r.Random Code)
+ (r/wrap (' [])))
+
+(def: #export primitive
+ (r.Random [Type Code])
+ (`` ($_ r.either
+ (~~ (do-template [<type> <code-wrapper> <value-gen>]
+ [(r.seq (r/wrap <type>) (r/map <code-wrapper> <value-gen>))]
+
+ [Top code.tuple (r.list +0 ..unit)]
+ [Bool code.bool r.bool]
+ [Nat code.nat r.nat]
+ [Int code.int r.int]
+ [Deg code.deg r.deg]
+ [Frac code.frac r.frac]
+ [Text code.text (r.unicode +5)]
+ )))))
+
(exception: (wrong-inference {expected Type} {inferred Type})
- (format "Expected: " (%type expected) "\n"
- "Inferred: " (%type inferred) "\n"))
+ (ex.report ["Expected" (%type expected)]
+ ["Inferred" (%type inferred)]))
(def: (infer-primitive expected-type analysis)
(-> Type (Meta Analysis) (e.Error Analysis))
@@ -34,30 +56,31 @@
(#e.Error error))))
(context: "Primitives"
- (<| (times +100)
- (`` ($_ seq
- (test "Can analyse unit."
- (|> (infer-primitive Top /.unit)
- (case> (^ (#e.Success (#analysis.Primitive (#analysis.Unit output))))
- (is? [] output)
-
- _
- false)))
- (~~ (do-template [<desc> <type> <tag> <random> <analyser>]
- [(do @
- [sample <random>]
- (test (format "Can analyse " <desc> ".")
- (|> (infer-primitive <type> (<analyser> sample))
- (case> (#e.Success (#analysis.Primitive (<tag> output)))
- (is? sample output)
-
- _
- false))))]
-
- ["bool" Bool #analysis.Bool r.bool /.bool]
- ["nat" Nat #analysis.Nat r.nat /.nat]
- ["int" Int #analysis.Int r.int /.int]
- ["deg" Deg #analysis.Deg r.deg /.deg]
- ["frac" Frac #analysis.Frac r.frac /.frac]
- ["text" Text #analysis.Text (r.unicode +5) /.text]
- ))))))
+ ($_ seq
+ (test "Can analyse unit."
+ (|> (infer-primitive Top (..analyse (' [])))
+ (case> (^ (#e.Success (#analysis.Primitive (#analysis.Unit output))))
+ (is? [] output)
+
+ _
+ false)))
+ (<| (times +100)
+ (`` ($_ seq
+ (~~ (do-template [<desc> <type> <tag> <random> <constructor>]
+ [(do @
+ [sample <random>]
+ (test (format "Can analyse " <desc> ".")
+ (|> (infer-primitive <type> (..analyse (<constructor> sample)))
+ (case> (#e.Success (#analysis.Primitive (<tag> output)))
+ (is? sample output)
+
+ _
+ false))))]
+
+ ["bool" Bool #analysis.Bool r.bool code.bool]
+ ["nat" Nat #analysis.Nat r.nat code.nat]
+ ["int" Int #analysis.Int r.int code.int]
+ ["deg" Deg #analysis.Deg r.deg code.deg]
+ ["frac" Frac #analysis.Frac r.frac code.frac]
+ ["text" Text #analysis.Text (r.unicode +5) code.text]
+ )))))))
diff --git a/stdlib/test/test/lux/lang/analysis/structure.lux b/stdlib/test/test/lux/lang/analysis/structure.lux
new file mode 100644
index 000000000..110717a0a
--- /dev/null
+++ b/stdlib/test/test/lux/lang/analysis/structure.lux
@@ -0,0 +1,292 @@
+(.module:
+ lux
+ (lux [io]
+ (control [monad #+ do]
+ pipe)
+ (data [bool "bool/" Eq<Bool>]
+ ["e" error]
+ [product]
+ [maybe]
+ [text]
+ text/format
+ (coll [list "list/" Functor<List>]
+ (set ["set" unordered])))
+ ["r" math/random "r/" Monad<Random>]
+ [macro]
+ (macro [code])
+ [lang]
+ (lang [type "type/" Eq<Type>]
+ (type ["tc" check])
+ [".L" module]
+ [".L" init]
+ [".L" analysis #+ Analysis]
+ (analysis [".A" type]
+ ["/" structure]
+ [".A" expression]))
+ test)
+ (// ["_." primitive]))
+
+(do-template [<name> <on-success> <on-error>]
+ [(def: <name>
+ (All [a] (-> (Meta a) Bool))
+ (|>> (macro.run (initL.compiler []))
+ (case> (#e.Success _)
+ <on-success>
+
+ _
+ <on-error>)))]
+
+ [check-succeeds true false]
+ [check-fails false true]
+ )
+
+(def: analyse (expressionA.analyser (:! lang.Eval [])))
+
+(def: (check-sum' size tag variant)
+ (-> Nat analysisL.Tag analysisL.Variant Bool)
+ (let [variant-tag (if (get@ #analysisL.right? variant)
+ (inc (get@ #analysisL.lefts variant))
+ (get@ #analysisL.lefts variant))]
+ (|> size dec (n/= tag)
+ (bool/= (get@ #analysisL.right? variant))
+ (and (n/= tag variant-tag)))))
+
+(def: (check-sum type size tag analysis)
+ (-> Type Nat analysisL.Tag (Meta Analysis) Bool)
+ (|> analysis
+ (typeA.with-type type)
+ (macro.run (initL.compiler []))
+ (case> (^multi (#e.Success sumA)
+ [(analysisL.variant sumA)
+ (#.Some variant)])
+ (check-sum' size tag variant)
+
+ _
+ false)))
+
+(def: (tagged module tags type)
+ (All [a] (-> Text (List moduleL.Tag) Type (Meta a) (Meta [Module a])))
+ (|>> (do macro.Monad<Meta>
+ [_ (moduleL.declare-tags tags false type)])
+ (moduleL.with-module +0 module)))
+
+(def: (check-variant module tags type size tag analysis)
+ (-> Text (List moduleL.Tag) Type Nat analysisL.Tag (Meta Analysis) Bool)
+ (|> analysis
+ (tagged module tags type)
+ (typeA.with-type type)
+ (macro.run (initL.compiler []))
+ (case> (^multi (#e.Success [_ sumA])
+ [(analysisL.variant sumA)
+ (#.Some variant)])
+ (check-sum' size tag variant)
+
+ _
+ false)))
+
+(def: (right-size? size)
+ (-> Nat (-> Analysis Bool))
+ (|>> analysisL.tuple list.size (n/= size)))
+
+(def: (check-record-inference module tags type size analysis)
+ (-> Text (List moduleL.Tag) Type Nat (Meta [Type Analysis]) Bool)
+ (|> analysis
+ (tagged module tags type)
+ (macro.run (initL.compiler []))
+ (case> (#e.Success [_ productT productA])
+ (and (type/= type productT)
+ (right-size? size productA))
+
+ _
+ false)))
+
+(context: "Sums"
+ (<| (times +100)
+ (do @
+ [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+ choice (|> r.nat (:: @ map (n/% size)))
+ primitives (r.list size _primitive.primitive)
+ +choice (|> r.nat (:: @ map (n/% (inc size))))
+ [_ +valueC] _primitive.primitive
+ #let [variantT (type.variant (list/map product.left primitives))
+ [valueT valueC] (maybe.assume (list.nth choice primitives))
+ +size (inc size)
+ +primitives (list.concat (list (list.take choice primitives)
+ (list [(#.Bound +1) +valueC])
+ (list.drop choice primitives)))
+ [+valueT +valueC] (maybe.assume (list.nth +choice +primitives))
+ +variantT (type.variant (list/map product.left +primitives))]]
+ ($_ seq
+ (test "Can analyse sum."
+ (check-sum variantT size choice
+ (/.sum ..analyse choice valueC)))
+ (test "Can analyse sum through bound type-vars."
+ (|> (do macro.Monad<Meta>
+ [[_ varT] (typeA.with-env tc.var)
+ _ (typeA.with-env
+ (tc.check varT variantT))]
+ (typeA.with-type varT
+ (/.sum ..analyse choice valueC)))
+ (macro.run (initL.compiler []))
+ (case> (^multi (#e.Success sumA)
+ [(analysisL.variant sumA)
+ (#.Some variant)])
+ (check-sum' size choice variant)
+
+ _
+ false)))
+ (test "Cannot analyse sum through unbound type-vars."
+ (|> (do macro.Monad<Meta>
+ [[_ varT] (typeA.with-env tc.var)]
+ (typeA.with-type varT
+ (/.sum ..analyse choice valueC)))
+ check-fails))
+ (test "Can analyse sum through existential quantification."
+ (|> (typeA.with-type (type.ex-q +1 +variantT)
+ (/.sum ..analyse +choice +valueC))
+ check-succeeds))
+ (test "Can analyse sum through universal quantification."
+ (let [check-outcome (if (not (n/= choice +choice))
+ check-succeeds
+ check-fails)]
+ (|> (typeA.with-type (type.univ-q +1 +variantT)
+ (/.sum ..analyse +choice +valueC))
+ check-outcome)))
+ ))))
+
+(context: "Products"
+ (<| (times +100)
+ (do @
+ [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+ primitives (r.list size _primitive.primitive)
+ choice (|> r.nat (:: @ map (n/% size)))
+ [_ +valueC] _primitive.primitive
+ #let [tupleT (type.tuple (list/map product.left primitives))
+ [singletonT singletonC] (|> primitives (list.nth choice) maybe.assume)
+ +primitives (list.concat (list (list.take choice primitives)
+ (list [(#.Bound +1) +valueC])
+ (list.drop choice primitives)))
+ +tupleT (type.tuple (list/map product.left +primitives))]]
+ ($_ seq
+ (test "Can analyse product."
+ (|> (typeA.with-type tupleT
+ (/.product ..analyse (list/map product.right primitives)))
+ (macro.run (initL.compiler []))
+ (case> (#e.Success tupleA)
+ (right-size? size tupleA)
+
+ _
+ false)))
+ (test "Can infer product."
+ (|> (typeA.with-inference
+ (/.product ..analyse (list/map product.right primitives)))
+ (macro.run (initL.compiler []))
+ (case> (#e.Success [_type tupleA])
+ (and (type/= tupleT _type)
+ (right-size? size tupleA))
+
+ _
+ false)))
+ (test "Can analyse pseudo-product (singleton tuple)"
+ (|> (typeA.with-type singletonT
+ (..analyse (` [(~ singletonC)])))
+ check-succeeds))
+ (test "Can analyse product through bound type-vars."
+ (|> (do macro.Monad<Meta>
+ [[_ varT] (typeA.with-env tc.var)
+ _ (typeA.with-env
+ (tc.check varT (type.tuple (list/map product.left primitives))))]
+ (typeA.with-type varT
+ (/.product ..analyse (list/map product.right primitives))))
+ (macro.run (initL.compiler []))
+ (case> (#e.Success tupleA)
+ (right-size? size tupleA)
+
+ _
+ false)))
+ (test "Can analyse product through existential quantification."
+ (|> (typeA.with-type (type.ex-q +1 +tupleT)
+ (/.product ..analyse (list/map product.right +primitives)))
+ check-succeeds))
+ (test "Cannot analyse product through universal quantification."
+ (|> (typeA.with-type (type.univ-q +1 +tupleT)
+ (/.product ..analyse (list/map product.right +primitives)))
+ check-fails))
+ ))))
+
+(context: "Tagged Sums"
+ (<| (times +100)
+ (do @
+ [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+ tags (|> (r.set text.Hash<Text> size (r.unicode +5)) (:: @ map set.to-list))
+ choice (|> r.nat (:: @ map (n/% size)))
+ other-choice (|> r.nat (:: @ map (n/% size)) (r.filter (|>> (n/= choice) not)))
+ primitives (r.list size _primitive.primitive)
+ module-name (r.unicode +5)
+ type-name (r.unicode +5)
+ #let [varT (#.Bound +1)
+ primitivesT (list/map product.left primitives)
+ [choiceT choiceC] (maybe.assume (list.nth choice primitives))
+ [other-choiceT other-choiceC] (maybe.assume (list.nth other-choice primitives))
+ variantT (type.variant primitivesT)
+ namedT (#.Named [module-name type-name] variantT)
+ named-polyT (|> (type.variant (list.concat (list (list.take choice primitivesT)
+ (list varT)
+ (list.drop (inc choice) primitivesT))))
+ (type.univ-q +1)
+ (#.Named [module-name type-name]))
+ choice-tag (maybe.assume (list.nth choice tags))
+ other-choice-tag (maybe.assume (list.nth other-choice tags))]]
+ ($_ seq
+ (test "Can infer tagged sum."
+ (|> (/.tagged-sum ..analyse [module-name choice-tag] choiceC)
+ (check-variant module-name tags namedT choice size)))
+ (test "Tagged sums specialize when type-vars get bound."
+ (|> (/.tagged-sum ..analyse [module-name choice-tag] choiceC)
+ (check-variant module-name tags named-polyT choice size)))
+ (test "Tagged sum inference retains universal quantification when type-vars are not bound."
+ (|> (/.tagged-sum ..analyse [module-name other-choice-tag] other-choiceC)
+ (check-variant module-name tags named-polyT other-choice size)))
+ (test "Can specialize generic tagged sums."
+ (|> (typeA.with-type variantT
+ (/.tagged-sum ..analyse [module-name other-choice-tag] other-choiceC))
+ (check-variant module-name tags named-polyT other-choice size)))
+ ))))
+
+(context: "Records"
+ (<| (times +100)
+ (do @
+ [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
+ tags (|> (r.set text.Hash<Text> size (r.unicode +5)) (:: @ map set.to-list))
+ primitives (r.list size _primitive.primitive)
+ module-name (r.unicode +5)
+ type-name (r.unicode +5)
+ choice (|> r.nat (:: @ map (n/% size)))
+ #let [varT (#.Bound +1)
+ tagsC (list/map (|>> [module-name] code.tag) tags)
+ primitivesT (list/map product.left primitives)
+ primitivesC (list/map product.right primitives)
+ tupleT (type.tuple primitivesT)
+ namedT (#.Named [module-name type-name] tupleT)
+ recordC (list.zip2 tagsC primitivesC)
+ named-polyT (|> (type.tuple (list.concat (list (list.take choice primitivesT)
+ (list varT)
+ (list.drop (inc choice) primitivesT))))
+ (type.univ-q +1)
+ (#.Named [module-name type-name]))]]
+ ($_ seq
+ (test "Can infer record."
+ (|> (typeA.with-inference
+ (/.record ..analyse recordC))
+ (check-record-inference module-name tags namedT size)))
+ (test "Records specialize when type-vars get bound."
+ (|> (typeA.with-inference
+ (/.record ..analyse recordC))
+ (check-record-inference module-name tags named-polyT size)))
+ (test "Can specialize generic records."
+ (|> (do macro.Monad<Meta>
+ [recordA (typeA.with-type tupleT
+ (/.record ..analyse recordC))]
+ (wrap [tupleT recordA]))
+ (check-record-inference module-name tags named-polyT size)))
+ ))))
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 12:43:29 +0000