aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/lang/analysis
diff options
context:
space:
mode:
Diffstat (limited to 'new-luxc/source/luxc/lang/analysis')
-rw-r--r--new-luxc/source/luxc/lang/analysis/case.lux23
-rw-r--r--new-luxc/source/luxc/lang/analysis/common.lux12
-rw-r--r--new-luxc/source/luxc/lang/analysis/function.lux24
-rw-r--r--new-luxc/source/luxc/lang/analysis/inference.lux80
-rw-r--r--new-luxc/source/luxc/lang/analysis/procedure/common.lux36
-rw-r--r--new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux12
-rw-r--r--new-luxc/source/luxc/lang/analysis/structure.lux41
7 files changed, 74 insertions, 154 deletions
diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux
index 5bf2e8ed1..ee4d4fcfa 100644
--- a/new-luxc/source/luxc/lang/analysis/case.lux
+++ b/new-luxc/source/luxc/lang/analysis/case.lux
@@ -47,13 +47,13 @@
(case caseT
(#;Var id)
(do meta;Monad<Meta>
- [? (&;with-type-env
- (tc;concrete? id))]
- (if ?
- (do @
- [caseT' (&;with-type-env
- (tc;read id))]
- (simplify-case-type caseT'))
+ [?caseT' (&;with-type-env
+ (tc;read id))]
+ (case ?caseT'
+ (#;Some caseT')
+ (simplify-case-type caseT')
+
+ _
(&;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT))))
(#;Named name unnamedT)
@@ -71,9 +71,12 @@
(do meta;Monad<Meta>
[funcT' (&;with-type-env
(do tc;Monad<Check>
- [? (tc;concrete? funcT-id)]
- (if ?
- (tc;read funcT-id)
+ [?funct' (tc;read funcT-id)]
+ (case ?funct'
+ (#;Some funct')
+ (wrap funct')
+
+ _
(tc;throw Cannot-Simplify-Type-For-Pattern-Matching (%type caseT)))))]
(simplify-case-type (#;Apply inputT funcT')))
diff --git a/new-luxc/source/luxc/lang/analysis/common.lux b/new-luxc/source/luxc/lang/analysis/common.lux
index b14524559..968ebd2ea 100644
--- a/new-luxc/source/luxc/lang/analysis/common.lux
+++ b/new-luxc/source/luxc/lang/analysis/common.lux
@@ -11,14 +11,12 @@
(lang analysis)))
(def: #export (with-unknown-type action)
- (All [a] (-> (Meta Analysis) (Meta [Type Analysis])))
+ (All [a] (-> (Meta a) (Meta [Type a])))
(do meta;Monad<Meta>
- [[var-id var-type] (&;with-type-env tc;var)
- analysis (&;with-expected-type var-type
- action)
- analysis-type (&;with-type-env
- (tc;clean var-id var-type))]
- (wrap [analysis-type analysis])))
+ [[_ varT] (&;with-type-env tc;var)
+ analysis (&;with-expected-type varT
+ action)]
+ (wrap [varT analysis])))
(exception: #export Variant-Tag-Out-Of-Bounds)
diff --git a/new-luxc/source/luxc/lang/analysis/function.lux b/new-luxc/source/luxc/lang/analysis/function.lux
index 2a9826683..6a4a33e48 100644
--- a/new-luxc/source/luxc/lang/analysis/function.lux
+++ b/new-luxc/source/luxc/lang/analysis/function.lux
@@ -50,29 +50,21 @@
(#;Var id)
(do @
- [? (&;with-type-env
- (tc;concrete? id))]
- (if ?
- (do @
- [expectedT' (&;with-type-env
- (tc;read id))]
- (recur expectedT'))
+ [?expectedT' (&;with-type-env
+ (tc;read id))]
+ (case ?expectedT'
+ (#;Some expectedT')
+ (recur expectedT')
+
+ _
## Inference
(do @
[[input-id inputT] (&;with-type-env tc;var)
[output-id outputT] (&;with-type-env tc;var)
#let [funT (#;Function inputT outputT)]
funA (recur funT)
- funT' (&;with-type-env
- (tc;clean output-id funT))
- concrete-input? (&;with-type-env
- (tc;concrete? input-id))
- funT'' (if concrete-input?
- (&;with-type-env
- (tc;clean input-id funT'))
- (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
_ (&;with-type-env
- (tc;check expectedT funT''))]
+ (tc;check expectedT funT))]
(wrap funA))
))
diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux
index 5152de0b6..8b04ac2b7 100644
--- a/new-luxc/source/luxc/lang/analysis/inference.lux
+++ b/new-luxc/source/luxc/lang/analysis/inference.lux
@@ -14,50 +14,22 @@
(analysis ["&;" common]))))
(exception: #export Cannot-Infer)
+(def: (cannot-infer type args)
+ (-> Type (List Code) Text)
+ (format " Type: " (%type type) "\n"
+ "Arguments:"
+ (|> args
+ list;enumerate
+ (list/map (function [[idx argC]]
+ (format "\n " (%n idx) " " (%code argC))))
+ (text;join-with ""))))
+
(exception: #export Cannot-Infer-Argument)
(exception: #export Smaller-Variant-Than-Expected)
(exception: #export Invalid-Type-Application)
(exception: #export Not-A-Record-Type)
(exception: #export Not-A-Variant-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
- (#;Primitive name params)
- (#;Primitive name (list/map (replace-var var-id bound-idx) params))
-
- (^template [<tag>]
- (<tag> left right)
- (<tag> (replace-var var-id bound-idx left)
- (replace-var var-id bound-idx right)))
- ([#;Sum]
- [#;Product]
- [#;Function]
- [#;Apply])
-
- (#;Var id)
- (if (n.= var-id id)
- (#;Bound bound-idx)
- type)
-
- (^template [<tag>]
- (<tag> env quantified)
- (<tag> (list/map (replace-var var-id bound-idx) env)
- (replace-var var-id (n.+ +2 bound-idx) quantified)))
- ([#;UnivQ]
- [#;ExQ])
-
- _
- type))
-
(def: (replace-bound bound-idx replacementT type)
(-> Nat Type Type Type)
(case type
@@ -110,18 +82,8 @@
(#;UnivQ _)
(do meta;Monad<Meta>
- [[var-id varT] (&;with-type-env tc;var)
- [outputT argsA] (general analyse (maybe;assume (type;apply (list varT) inferT)) args)]
- (do @
- [? (&;with-type-env
- (tc;concrete? var-id))
- ## Quantify over the type if genericity/parametricity
- ## is discovered.
- outputT' (if ?
- (&;with-type-env
- (tc;clean var-id outputT))
- (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))]
- (wrap [outputT' argsA])))
+ [[var-id varT] (&;with-type-env tc;var)]
+ (general analyse (maybe;assume (type;apply (list varT) inferT)) args))
(#;ExQ _)
(do meta;Monad<Meta>
@@ -155,14 +117,18 @@
(analyse argC)))]
(wrap [outputT' (list& argA args'A)]))
+ (#;Var infer-id)
+ (do meta;Monad<Meta>
+ [?inferT' (&;with-type-env (tc;read infer-id))]
+ (case ?inferT'
+ (#;Some inferT')
+ (general analyse inferT' args)
+
+ _
+ (&;throw Cannot-Infer (cannot-infer inferT args))))
+
_
- (&;throw Cannot-Infer (format " Type: " (%type inferT) "\n"
- "Arguments:"
- (|> args
- list;enumerate
- (list/map (function [[idx argC]]
- (format "\n " (%n idx) " " (%code argC))))
- (text;join-with "")))))
+ (&;throw Cannot-Infer (cannot-infer inferT args)))
))
## Turns a record type into the kind of function type suitable for inference.
diff --git a/new-luxc/source/luxc/lang/analysis/procedure/common.lux b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
index fff5de504..3965e78ba 100644
--- a/new-luxc/source/luxc/lang/analysis/procedure/common.lux
+++ b/new-luxc/source/luxc/lang/analysis/procedure/common.lux
@@ -141,42 +141,6 @@
[lux//check typeA;analyse-check]
[lux//coerce typeA;analyse-coerce])
-(def: (clean-type inputT)
- (-> Type (tc;Check Type))
- (case inputT
- (#;Primitive name paramsT+)
- (do tc;Monad<Check>
- [paramsT+' (monad;map @ clean-type paramsT+)]
- (wrap (#;Primitive name paramsT+')))
-
- (^or #;Void #;Unit (#;Bound _) (#;Ex _) (#;Named _))
- (:: tc;Monad<Check> wrap inputT)
-
- (^template [<tag>]
- (<tag> leftT rightT)
- (do tc;Monad<Check>
- [leftT' (clean-type leftT)
- rightT' (clean-type rightT)]
- (wrap (<tag> leftT' rightT'))))
- ([#;Sum] [#;Product] [#;Function] [#;Apply])
-
- (#;Var id)
- (do tc;Monad<Check>
- [? (tc;concrete? id)]
- (if ?
- (do @
- [actualT (tc;read id)]
- (clean-type actualT))
- (wrap inputT)))
-
- (^template [<tag>]
- (<tag> envT+ unquantifiedT)
- (do tc;Monad<Check>
- [envT+' (monad;map @ clean-type envT+)]
- (wrap (<tag> envT+' unquantifiedT))))
- ([#;UnivQ] [#;ExQ])
- ))
-
(def: (lux//check//type proc)
(-> Text Proc)
(function [analyse eval args]
diff --git a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
index 39ca0eb43..cd5fdc7bb 100644
--- a/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
+++ b/new-luxc/source/luxc/lang/analysis/procedure/host.jvm.lux
@@ -305,9 +305,9 @@
_ (&;infer varT)
arrayA (&;with-expected-type (type (Array varT))
(analyse arrayC))
- elemT (&;with-type-env
- (tc;read var-id))
- [elemT elem-class] (box-array-element-type elemT)
+ ?elemT (&;with-type-env
+ (tc;read var-id))
+ [elemT elem-class] (box-array-element-type (maybe;default varT ?elemT))
idxA (&;with-expected-type Nat
(analyse idxC))]
(wrap (la;procedure proc (list (code;text elem-class) idxA arrayA))))
@@ -325,9 +325,9 @@
_ (&;infer (type (Array varT)))
arrayA (&;with-expected-type (type (Array varT))
(analyse arrayC))
- elemT (&;with-type-env
- (tc;read var-id))
- [valueT elem-class] (box-array-element-type elemT)
+ ?elemT (&;with-type-env
+ (tc;read var-id))
+ [valueT elem-class] (box-array-element-type (maybe;default varT ?elemT))
idxA (&;with-expected-type Nat
(analyse idxC))
valueA (&;with-expected-type valueT
diff --git a/new-luxc/source/luxc/lang/analysis/structure.lux b/new-luxc/source/luxc/lang/analysis/structure.lux
index e1f4de1d7..1f1ef15d7 100644
--- a/new-luxc/source/luxc/lang/analysis/structure.lux
+++ b/new-luxc/source/luxc/lang/analysis/structure.lux
@@ -1,17 +1,13 @@
(;module:
lux
(lux (control [monad #+ do]
- ["ex" exception #+ exception:]
- pipe)
- [function]
- (concurrency ["A" atom])
+ ["ex" exception #+ exception:])
(data [ident]
[number]
[product]
[maybe]
(coll [list "list/" Functor<List>]
[dict #+ Dict])
- [text]
text/format)
[meta]
(meta [code]
@@ -63,20 +59,21 @@
(#;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)))
+ [?expectedT' (&;with-type-env
+ (tc;read id))]
+ (case ?expectedT'
+ (#;Some expectedT')
+ (&;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)))))
+ " Type: " (%type expectedT)))
+ ))
(^template [<tag> <instancer>]
(<tag> _)
@@ -166,14 +163,14 @@
(#;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)))
+ [?expectedT' (&;with-type-env
+ (tc;read id))]
+ (case ?expectedT'
+ (#;Some expectedT')
+ (&;with-expected-type expectedT'
+ (analyse-product analyse membersC))
+
+ _
## Must do inference...
(do @
[membersTA (monad;map @ (|>. analyse &common;with-unknown-type)