From 8f88e4bf4b380e2f09d046fbef05fca452eae62c Mon Sep 17 00:00:00 2001
From: Eduardo Julian
Date: Sat, 20 May 2017 18:29:24 -0400
Subject: WIP - Added analysis and type-inference for records and tagged
 variants. - Extracted inference code to a separate module for better reuse.

---
 new-luxc/source/luxc/analyser/function.lux | 108 ++++-------------------------
 1 file changed, 15 insertions(+), 93 deletions(-)

(limited to 'new-luxc/source/luxc/analyser/function.lux')

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)))))
-- 
cgit v1.2.3