aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/analyser/function.lux
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/analyser/function.lux108
1 files changed, 15 insertions, 93 deletions
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 44deec45b..838de4181 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -10,43 +10,10 @@
(luxc ["&" base]
(lang ["la" analysis #+ Analysis])
["&;" env]
- (analyser ["&;" common])))
+ (analyser ["&;" common]
+ ["&;" inference])))
## [Analysers]
-(def: (bind-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))
-
- (^template [<tag>]
- (<tag> left right)
- (<tag> (bind-var var-id bound-idx left)
- (bind-var var-id bound-idx right)))
- ([#;Sum]
- [#;Product]
- [#;Function]
- [#;App])
-
- (#;Var id)
- (if (n.= var-id id)
- (#;Bound bound-idx)
- type)
-
- (^template [<tag>]
- (<tag> env quantified)
- (<tag> (L/map (bind-var var-id bound-idx) env)
- (bind-var var-id (n.+ +2 bound-idx) quantified)))
- ([#;UnivQ]
- [#;ExQ])
-
- (#;Named name unnamedT)
- (#;Named name
- (bind-var var-id bound-idx unnamedT))
-
- _
- type))
-
(def: #export (analyse-function analyse func-name arg-name body)
(-> &;Analyser Text Text Code (Lux Analysis))
(do Monad<Lux>
@@ -103,7 +70,7 @@
funT'' (if concrete-input?
(&;within-type-env
(TC;clean input-id funT'))
- (wrap (#;UnivQ (list) (bind-var input-id +1 funT'))))
+ (wrap (#;UnivQ (list) (&inference;bind-var input-id +1 funT'))))
_ (&;within-type-env
(TC;check expected funT''))]
(wrap =function))
@@ -121,62 +88,17 @@
(&;fail "")
)))))
-(def: (analyse-apply' analyse funcT args)
- (-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
- (case args
- #;Nil
- (:: Monad<Lux> wrap [funcT (list)])
-
- (#;Cons arg args')
- (&;with-stacked-errors
- (function [_] (format "Cannot apply function " (%type funcT)
- " to args: " (|> args (L/map %code) (text;join-with " "))))
- (case funcT
- (#;Named name unnamedT)
- (analyse-apply' analyse unnamedT args)
-
- (#;UnivQ _)
- (&common;with-var
- (function [[var-id varT]]
- (do Monad<Lux>
- [[outputT argsA] (analyse-apply' analyse (assume (type;apply-type funcT varT)) args)]
- (do @
- [? (&;within-type-env
- (TC;bound? var-id))
- outputT' (if ?
- (&;within-type-env
- (TC;clean var-id outputT))
- (wrap (#;UnivQ (list) (bind-var var-id +1 outputT))))]
- (wrap [outputT' argsA])))))
-
- (#;ExQ _)
- (do Monad<Lux>
- [[ex-id exT] (&;within-type-env
- TC;existential)]
- (analyse-apply' analyse (assume (type;apply-type funcT exT)) args))
-
- (#;Function inputT outputT)
- (do Monad<Lux>
- [[outputT' args'A] (analyse-apply' analyse outputT args')
- argA (&;with-stacked-errors
- (function [_] (format "Expected type: " (%type inputT) "\n"
- " For argument: " (%code arg)))
- (&;with-expected-type inputT
- (analyse arg)))]
- (wrap [outputT' (list& argA args'A)]))
-
- _
- (&;fail (format "Cannot apply a non-function: " (%type funcT)))))
- ))
-
(def: #export (analyse-apply analyse funcT funcA args)
(-> &;Analyser Type Analysis (List Code) (Lux Analysis))
- (do Monad<Lux>
- [expected macro;expected-type
- [applyT argsA] (analyse-apply' analyse funcT args)
- _ (&;within-type-env
- (TC;check expected applyT))]
- (wrap (L/fold (function [arg func]
- (#la;Apply arg func))
- funcA
- argsA))))
+ (&;with-stacked-errors
+ (function [_] (format "Cannot apply function " (%type funcT)
+ " to args: " (|> args (L/map %code) (text;join-with " "))))
+ (do Monad<Lux>
+ [expected macro;expected-type
+ [applyT argsA] (&inference;apply-function analyse funcT args)
+ _ (&;within-type-env
+ (TC;check expected applyT))]
+ (wrap (L/fold (function [arg func]
+ (#la;Apply arg func))
+ funcA
+ argsA)))))