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/inference.lux | 90 +++++++++++++++++++++++++++++
 1 file changed, 90 insertions(+)
 create mode 100644 new-luxc/source/luxc/analyser/inference.lux

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

diff --git a/new-luxc/source/luxc/analyser/inference.lux b/new-luxc/source/luxc/analyser/inference.lux
new file mode 100644
index 000000000..824071ab3
--- /dev/null
+++ b/new-luxc/source/luxc/analyser/inference.lux
@@ -0,0 +1,90 @@
+(;module:
+  lux
+  (lux (control monad)
+       (data text/format
+             (coll [list "L/" Functor<List>]))
+       [macro #+ Monad<Lux>]
+       [type]
+       (type ["TC" check]))
+  (luxc ["&" base]
+        (lang ["la" analysis #+ Analysis])
+        (analyser ["&;" common])))
+
+(def: #export (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 (apply-function analyse funcT args)
+  (-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
+  (case args
+    #;Nil
+    (:: Monad<Lux> wrap [funcT (list)])
+    
+    (#;Cons arg args')
+    (case funcT
+      (#;Named name unnamedT)
+      (apply-function analyse unnamedT args)
+
+      (#;UnivQ _)
+      (&common;with-var
+        (function [[var-id varT]]
+          (do Monad<Lux>
+            [[outputT argsA] (apply-function 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)]
+        (apply-function analyse (assume (type;apply-type funcT exT)) args))
+
+      (#;Function inputT outputT)
+      (do Monad<Lux>
+        [[outputT' args'A] (apply-function 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))))
+    ))
-- 
cgit v1.2.3