WIP

- Simplified the Analysis type, by removing all meta-data.
- Added analysis of function calls.
- Added analysis of common Lux procedures.
- Lots of refactoring.

1 files changed, 188 insertions, 0 deletions

diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
new file mode 100644
index 000000000..17441b760
--- /dev/null
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -0,0 +1,188 @@
+(;module:
+  lux
+  (lux (control monad)
+       (data ["E" error]
+             [text]
+             text/format
+             (coll [list "L/" Fold<List> Monoid<List> Monad<List>]))
+       [macro #+ Monad<Lux>]
+       [type]
+       (type ["TC" check]))
+  (luxc ["&" base]
+        (lang ["la" analysis #+ Analysis])
+        ["&;" env]
+        (analyser ["&;" common])))
+
+## [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>
+    [expected macro;expected-type]
+    (&;with-stacked-errors
+      (function [_] (format "Functions require function types: " (type;to-text expected)))
+      (case expected
+        (#;Named name unnamedT)
+        (&;with-expected-type unnamedT
+          (analyse-function analyse func-name arg-name body))
+
+        (#;App funT argT)
+        (do @
+          [fully-applied (case (type;apply-type funT argT)
+                           (#;Some value)
+                           (wrap value)
+
+                           #;None
+                           (&;fail (format "Cannot apply type " (%type funT) " to  type " (%type argT))))]
+          (&;with-expected-type fully-applied
+            (analyse-function analyse func-name arg-name body)))
+        
+        (#;UnivQ _)
+        (do @
+          [[var-id var] (&;within-type-env
+                         TC;existential)]
+          (&;with-expected-type (assume (type;apply-type expected var))
+            (analyse-function analyse func-name arg-name body)))
+
+        (#;ExQ _)
+        (&common;with-var
+          (function [[var-id var]]
+            (&;with-expected-type (assume (type;apply-type expected var))
+              (analyse-function analyse func-name arg-name body))))
+        
+        (#;Var id)
+        (do @
+          [? (&;within-type-env
+              (TC;bound? id))]
+          (if ?
+            (do @
+              [expected' (&;within-type-env
+                          (TC;read-var id))]
+              (&;with-expected-type expected'
+                (analyse-function analyse func-name arg-name body)))
+            ## Inference
+            (&common;with-var
+              (function [[input-id inputT]]
+                (&common;with-var
+                  (function [[output-id outputT]]
+                    (do @
+                      [#let [funT (#;Function inputT outputT)]
+                       =function (&;with-expected-type funT
+                                   (analyse-function analyse func-name arg-name body))
+                       funT' (&;within-type-env
+                              (TC;clean output-id funT))
+                       concrete-input? (&;within-type-env
+                                        (TC;bound? input-id))
+                       funT'' (if concrete-input?
+                                (&;within-type-env
+                                 (TC;clean input-id funT'))
+                                (wrap (#;UnivQ (list) (bind-var input-id +1 funT'))))
+                       _ (&;within-type-env
+                          (TC;check expected funT''))]
+                      (wrap =function))
+                    ))))))
+
+        (#;Function inputT outputT)
+        (<| (:: @ map (|>. #la;Function))
+            &;with-scope
+            (&env;with-local [func-name expected])
+            (&env;with-local [arg-name inputT])
+            (&;with-expected-type outputT)
+            (analyse body))
+        
+        _
+        (&;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))))