Finishing the meta-compiler [Part 2]

5 files changed, 271 insertions, 123 deletions

diff --git a/stdlib/source/test/lux/target/python.lux b/stdlib/source/test/lux/target/python.lux
index 39c51b2a7..6eed5ecab 100644
--- a/stdlib/source/test/lux/target/python.lux
+++ b/stdlib/source/test/lux/target/python.lux
@@ -324,6 +324,31 @@
                                         (list (/.float float/0) (/.float float/1) (/.float float/2)))))
         )))
 
+(def: test|var
+  Test
+  (do [! random.monad]
+    [expected/0 random.safe_frac
+     expected/1 random.safe_frac
+     choice (# ! each (n.% 2) random.nat)
+     .let [expected/? (case choice
+                        0 expected/0
+                        _ expected/1)]
+     $var (# ! each (|>> %.nat (format "v") /.var) random.nat)
+     $choice (# ! each (|>> %.nat (format "c") /.var) random.nat)]
+    ($_ _.and
+        (_.cover [/.Single /.SVar /.var]
+                 (expression (|>> (:as Frac) (f.= expected/0))
+                             (/.apply/* (/.lambda (list $var) $var)
+                                        (list (/.float expected/0)))))
+        (_.cover [/.Poly /.PVar /.poly]
+                 (expression (|>> (:as Frac) (f.= expected/?))
+                             (/.apply/* (/.lambda (list $choice (/.poly $var))
+                                                  (/.item $choice $var))
+                                        (list (/.int (.int choice))
+                                              (/.float expected/0)
+                                              (/.float expected/1)))))
+        )))
+
 (def: test|expression
   Test
   (do [! random.monad]
@@ -335,6 +360,8 @@
             (_.for [/.Computation]
                    ..test|computation)
             ..test|function
+            (_.for [/.Var]
+                   ..test|var)
             ))))
 
 (def: .public test
diff --git a/stdlib/source/test/lux/tool.lux b/stdlib/source/test/lux/tool.lux
index 0f42f81db..c9a5cfb7c 100644
--- a/stdlib/source/test/lux/tool.lux
+++ b/stdlib/source/test/lux/tool.lux
@@ -17,7 +17,8 @@
       ["[1]/[0]" analysis "_"
        ["[1]/[0]" simple]
        ["[1]/[0]" complex]
-       ["[1]/[0]" reference]]
+       ["[1]/[0]" reference]
+       ["[1]/[0]" function]]
       ... ["[1]/[0]" synthesis]
       ]]]
    ["[1][0]" meta "_"
@@ -41,6 +42,7 @@
       /phase/analysis/simple.test
       /phase/analysis/complex.test
       /phase/analysis/reference.test
+      /phase/analysis/function.test
       ... /syntax.test
       ... /synthesis.test
       ))
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
index fa3df9c67..97bdb7a54 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/analysis/inference.lux
@@ -78,7 +78,7 @@
     {try.#Failure error}
     (text.contains? (value@ exception.#label exception) error)))
 
-(def: simple_parameter
+(def: .public simple_parameter
   (Random [Type Code])
   (`` ($_ random.either
           (~~ (template [<type> <random> <code>]
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
index f559e98c4..ed111c5e4 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/complex.lux
@@ -230,7 +230,6 @@
                    (list.item tag)
                    (maybe.else ""))]]
     ($_ _.and
-        ..test|sum
         (_.cover [/.variant]
                  (let [expected_variant? (: (-> Symbol Bit)
                                             (function (_ tag)
diff --git a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
index 815b488fe..50fbc1c50 100644
--- a/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
+++ b/stdlib/source/test/lux/tool/compiler/language/lux/phase/analysis/function.lux
@@ -1,133 +1,253 @@
 (.using
+ [library
   [lux "*"
-   [abstract
-    ["[0]" monad {"+" do}]]
-   [data
-    ["%" text/format {"+" format}]]
-   ["r" math/random {"+" Random}]
    ["_" test {"+" Test}]
+   [abstract
+    [monad {"+" do}]]
    [control
-    pipe
-    ["[0]" maybe]
-    ["[0]" try]]
+    [pipe {"+" case>}]
+    ["[0]" function]
+    ["[0]" try ("[1]#[0]" functor)]
+    ["[0]" exception]]
    [data
     ["[0]" product]
-    ["[0]" text ("[1]#[0]" equivalence)]
-    [number
-     ["n" nat]]
+    ["[0]" text
+     ["%" format]]
     [collection
-     ["[0]" list ("[1]#[0]" functor)]]]
-   ["[0]" type]
-   ["[0]" macro
+     ["[0]" list]]]
+   [macro
     ["[0]" code]]
+   [math
+    ["[0]" random]
+    [number
+     ["n" nat]]]
    [meta
-    ["[0]" symbol]]]
-  [//
-   ["_[0]" primitive]
-   ["_[0]" structure]]
-  [\\
-   ["[0]" /
-    ["/[1]" //
-     ["[1][0]" module]
-     ["[1][0]" type]
-     ["/[1]" // "_"
-      ["/[1]" //
-       ["[1][0]" analysis {"+" Analysis Operation}]
-       [///
-        ["[1][0]" reference]
-        ["[0]" phase]
-        [meta
-         ["[0]" archive]]]]]]]])
-
-(def: (check_apply expectedT num_args analysis)
-  (-> Type Nat (Operation Analysis) Bit)
-  (|> analysis
-      (//type.with_type expectedT)
-      (phase.result _primitive.state)
-      (case> {try.#Success applyA}
-             (let [[funcA argsA] (////analysis.application applyA)]
-               (n.= num_args (list.size argsA)))
-
-             {try.#Failure _}
-             false)))
-
-(def: abstraction
-  (do r.monad
-    [func_name (r.unicode 5)
-     arg_name (|> (r.unicode 5) (r.only (|>> (text#= func_name) not)))
-     [outputT outputC] _primitive.primitive
-     [inputT _] _primitive.primitive
-     .let [g!arg (code.local_symbol arg_name)]]
-    (<| (_.context (%.symbol (symbol /.function)))
-        ($_ _.and
-            (_.test "Can analyse function."
-                    (and (|> (//type.with_type (All (_ a) (-> a outputT))
-                               (/.function _primitive.phase func_name arg_name archive.empty outputC))
-                             _structure.check_succeeds)
-                         (|> (//type.with_type (All (_ a) (-> a a))
-                               (/.function _primitive.phase func_name arg_name archive.empty g!arg))
-                             _structure.check_succeeds)))
-            (_.test "Generic functions can always be specialized."
-                    (and (|> (//type.with_type (-> inputT outputT)
-                               (/.function _primitive.phase func_name arg_name archive.empty outputC))
-                             _structure.check_succeeds)
-                         (|> (//type.with_type (-> inputT inputT)
-                               (/.function _primitive.phase func_name arg_name archive.empty g!arg))
-                             _structure.check_succeeds)))
-            (_.test "The function's name is bound to the function's type."
-                    (|> (//type.with_type (Rec self (-> inputT self))
-                          (/.function _primitive.phase func_name arg_name archive.empty (code.local_symbol func_name)))
-                        _structure.check_succeeds))
-            ))))
+    ["[0]" symbol "_"
+     ["$[1]" \\test]]]
+   ["[0]" type ("[1]#[0]" equivalence)
+    ["$[1]" \\test]
+    ["[0]" check]]]]
+ [\\library
+  ["[0]" /
+   ["/[1]" //
+    [//
+     ["[1][0]" extension
+      ["[1]/[0]" analysis "_"
+       ["[1]" lux]]]
+     [//
+      ["[1][0]" analysis {"+" Analysis}
+       [evaluation {"+" Eval}]
+       ["[2][0]" macro]
+       ["[2][0]" scope]
+       ["[2][0]" module]
+       ["[2][0]" type
+        ["$[1]" \\test]]
+       ["[2][0]" inference "_"
+        ["$[1]" \\test]]]
+      [///
+       ["[1][0]" phase ("[1]#[0]" monad)]
+       [meta
+        ["[0]" archive]]]]]]]])
 
-(def: apply
-  (do [! r.monad]
-    [full_args (|> r.nat (# ! each (|>> (n.% 10) (n.max 2))))
-     partial_args (|> r.nat (# ! each (n.% full_args)))
-     var_idx (|> r.nat (# ! each (|>> (n.% full_args) (n.max 1))))
-     inputsTC (r.list full_args _primitive.primitive)
-     .let [inputsT (list#each product.left inputsTC)
-           inputsC (list#each product.right inputsTC)]
-     [outputT outputC] _primitive.primitive
-     .let [funcT (type.function inputsT outputT)
-           partialT (type.function (list.after partial_args inputsT) outputT)
-           varT {.#Parameter 1}
-           polyT (<| (type.univ_q 1)
-                     (type.function (list.together (list (list.first var_idx inputsT)
-                                                         (list varT)
-                                                         (list.after (++ var_idx) inputsT))))
-                     varT)
-           poly_inputT (maybe.trusted (list.item var_idx inputsT))
-           partial_poly_inputsT (list.after (++ var_idx) inputsT)
-           partial_polyT1 (<| (type.function partial_poly_inputsT)
-                              poly_inputT)
-           partial_polyT2 (<| (type.univ_q 1)
-                              (type.function {.#Item varT partial_poly_inputsT})
-                              varT)
-           dummy_function {////analysis.#Function (list) {////analysis.#Reference (////reference.local 1)}}]]
-    (<| (_.context (%.symbol (symbol /.apply)))
-        ($_ _.and
-            (_.test "Can analyse monomorphic type application."
-                    (|> (/.apply _primitive.phase inputsC funcT dummy_function archive.empty (' []))
-                        (check_apply outputT full_args)))
-            (_.test "Can partially apply functions."
-                    (|> (/.apply _primitive.phase (list.first partial_args inputsC) funcT dummy_function archive.empty (' []))
-                        (check_apply partialT partial_args)))
-            (_.test "Can apply polymorphic functions."
-                    (|> (/.apply _primitive.phase inputsC polyT dummy_function archive.empty (' []))
-                        (check_apply poly_inputT full_args)))
-            (_.test "Polymorphic partial application propagates found type-vars."
-                    (|> (/.apply _primitive.phase (list.first (++ var_idx) inputsC) polyT dummy_function archive.empty (' []))
-                        (check_apply partial_polyT1 (++ var_idx))))
-            (_.test "Polymorphic partial application preserves quantification for type-vars."
-                    (|> (/.apply _primitive.phase (list.first var_idx inputsC) polyT dummy_function archive.empty (' []))
-                        (check_apply partial_polyT2 var_idx)))
-            ))))
+(def: (eval archive type term)
+  Eval
+  (//phase#in []))
+
+(def: (expander macro inputs state)
+  //macro.Expander
+  {try.#Success ((.macro macro) inputs state)})
+
+(def: analysis
+  //analysis.Phase
+  (//.phase ..expander))
+
+(def: test|function
+  Test
+  (do [! random.monad]
+    [lux $//type.random_state
+     .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+                  //extension.#state lux]]
+     input/0 ($type.random 0)
+     input/1 ($type.random 0)
+     function/0 (random.ascii/lower 1)
+     function/1 (random.ascii/lower 2)
+     argument/0 (random.ascii/lower 3)
+     argument/1 (random.ascii/lower 4)
+     module/0 (random.ascii/lower 5)
+     [output/0 term/0] $//inference.simple_parameter
+     [output/1 term/1] (random.only (|>> product.left (same? output/0) not)
+                                    $//inference.simple_parameter)
+     name/0 ($symbol.random 1 1)
+     .let [$function/0 (code.local_symbol function/0)
+           $function/1 (code.local_symbol function/1)
+           $argument/0 (code.local_symbol argument/0)
+           $argument/1 (code.local_symbol argument/1)]]
+    ($_ _.and
+        (_.cover [/.function]
+                 (let [function?' (: (-> Type Code (-> [(List Analysis) Analysis] Bit) Bit)
+                                     (function (_ function_type output_term ?)
+                                       (|> (do //phase.monad
+                                             [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                                             output_term)
+                                                           (//type.expecting function_type))]
+                                             (in (case analysis
+                                                   {//analysis.#Function it}
+                                                   (? it)
+
+                                                   _
+                                                   false)))
+                                           (//module.with 0 module/0)
+                                           (//phase#each product.right)
+                                           (//phase.result state)
+                                           (try.else false))))
+                       function? (: (-> Type Code Bit)
+                                    (function (_ function_type output_term)
+                                      (function?' function_type output_term (function.constant true))))
+                       inferring? (: (-> Type Code Bit)
+                                     (function (_ :expected: term)
+                                       (|> (do //phase.monad
+                                             [[:actual: analysis] (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                                                        term)
+                                                                      //type.inferring)]
+                                             (in (case analysis
+                                                   {//analysis.#Function [actual_env actual_body]}
+                                                   (type#= :expected: :actual:)
+
+                                                   _
+                                                   false)))
+                                           (//module.with 0 module/0)
+                                           (//phase#each product.right)
+                                           (//phase.result state)
+                                           (try.else false))))]
+                   (and (function? (-> input/0 output/0) term/0)
+                        (function? (-> input/0 input/0) $argument/0)
+
+                        (function? {.#Named name/0 (-> input/0 output/0)} term/0)
+                        
+                        (function? (All (_ a) (-> a a)) $argument/0)
+                        (function? (Ex (_ a) (-> a a)) $argument/0)
+                        (function? (Ex (_ a) (-> input/0 a)) term/0)
+                        (function? (Ex (_ a) (-> a a)) term/0)
+                        (function? (Rec self (-> input/0 self)) $function/0)
+
+                        (function? (type ((All (_ a) (-> a a)) output/0)) term/0)
+                        (not (function? (type ((All (_ a) (-> a a)) output/1)) term/0))
+
+                        (function? (type ((Ex (_ a) (-> a a)) output/0)) term/0)
+                        (not (function? (type ((Ex (_ a) (-> a a)) output/1)) term/0))
+
+                        (function?' (-> input/0 input/1 input/0) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/0)))
+                                    (function (_ [outer body])
+                                      (and (list.empty? outer)
+                                           (case body
+                                             {//analysis.#Function [inner body]}
+                                             (n.= 1 (list.size inner))
+
+                                             _
+                                             false))))
+                        (function?' (-> input/0 input/1 input/1) (` ([(~ $function/1) (~ $argument/1)] (~ $argument/1)))
+                                    (function (_ [outer body])
+                                      (and (list.empty? outer)
+                                           (case body
+                                             {//analysis.#Function [inner body]}
+                                             (n.= 0 (list.size inner))
+
+                                             _
+                                             false))))
+
+                        (|> (do //phase.monad
+                              [[@var :var:] (//type.check check.var)
+                               _ (//type.check (check.check :var: (-> input/0 output/0)))
+                               analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                              term/0)
+                                            (//type.expecting :var:))]
+                              (in (case analysis
+                                    {//analysis.#Function [actual_env actual_body]}
+                                    true
+
+                                    _
+                                    false)))
+                            (//module.with 0 module/0)
+                            (//phase#each product.right)
+                            (//phase.result state)
+                            (try.else false))
+                        
+                        (inferring? (All (_ a) (-> a output/0)) term/0)
+                        (inferring? (All (_ a) (-> a a)) $argument/0)
+                        (inferring? (All (_ @0) (-> @0 @0 (And .Bit @0)))
+                                    (` ([(~ $function/1) (~ $argument/1)]
+                                        [("lux is" (~ $argument/0) (~ $argument/1))
+                                         (~ $argument/1)]))))))
+        (_.cover [/.cannot_analyse]
+                 (|> (do //phase.monad
+                       [analysis (|> (/.function ..analysis function/0 argument/0 archive.empty
+                                       term/1)
+                                     (//type.expecting (-> input/0 output/0)))]
+                       (in (case analysis
+                             {//analysis.#Function [actual_env actual_body]}
+                             true
+
+                             _
+                             false)))
+                     (//module.with 0 module/0)
+                     (//phase#each product.right)
+                     (//phase.result state)
+                     (exception.otherwise (text.contains? (value@ exception.#label /.cannot_analyse)))))
+        )))
 
 (def: .public test
   Test
-  (<| (_.context (symbol.module (symbol /._)))
-      ($_ _.and
-          ..abstraction
-          ..apply
-          )))
+  (<| (_.covering /._)
+      (do [! random.monad]
+        [lux $//type.random_state
+         .let [state [//extension.#bundle (//extension/analysis.bundle ..eval)
+                      //extension.#state lux]]
+         [input/0 term/0] $//inference.simple_parameter
+         [input/1 term/1] $//inference.simple_parameter
+         output/0 ($type.random 0)
+         module/0 (random.ascii/lower 1)]
+        ($_ _.and
+            ..test|function
+            (_.cover [/.apply]
+                     (let [reification? (: (-> Type (List Code) Type Bit)
+                                           (function (_ :abstraction: terms :expected:)
+                                             (|> (do //phase.monad
+                                                   [[:actual: analysis] (|> (/.apply ..analysis terms
+                                                                                     :abstraction:
+                                                                                     (//analysis.unit)
+                                                                                     archive.empty
+                                                                                     (' []))
+                                                                            //type.inferring)]
+                                                   (in (and (check.subsumes? :expected: :actual:)
+                                                            (case analysis
+                                                              {//analysis.#Apply _}
+                                                              true
+
+                                                              _
+                                                              false))))
+                                                 (//module.with 0 module/0)
+                                                 (//phase#each product.right)
+                                                 (//phase.result state)
+                                                 (try.else false))))]
+                       (and (reification? (-> input/0 input/1 output/0) (list term/0 term/1) output/0)
+                            (reification? (-> input/0 input/1 output/0) (list term/0) (-> input/1 output/0))
+                            (reification? (All (_ a) (-> a a)) (list term/0) input/0)
+                            (reification? (All (_ a) (-> a a a)) (list term/0) (-> input/0 input/0))
+                            (reification? (All (_ a) (-> input/0 a)) (list term/0) .Nothing)
+                            (reification? (All (_ a b) (-> a b a)) (list term/0) (All (_ b) (-> b input/0)))
+                            (reification? (Ex (_ a) (-> a input/0)) (list (` ("lux io error" ""))) input/0)
+                            (reification? (Ex (_ a) (-> input/0 a)) (list term/0) .Any))))
+            (_.cover [/.cannot_apply]
+                     (|> (do //phase.monad
+                           [_ (|> (/.apply ..analysis (list term/1 term/0)
+                                           (-> input/0 input/1 output/0)
+                                           (//analysis.unit)
+                                           archive.empty
+                                           (' []))
+                                  (//type.expecting output/0))]
+                           (in false))
+                         (//module.with 0 module/0)
+                         (//phase#each product.right)
+                         (//phase.result state)
+                         (exception.otherwise (text.contains? (value@ exception.#label /.cannot_apply)))))
+            ))))