- Implemented some synthesis algorithms and tests for primitives, structures, procedures and function application.

- Some refactoring.

13 files changed, 241 insertions, 50 deletions

diff --git a/new-luxc/test/test/luxc/analyser/case.lux b/new-luxc/test/test/luxc/analyser/case.lux
index f43625825..218ebc0cd 100644
--- a/new-luxc/test/test/luxc/analyser/case.lux
+++ b/new-luxc/test/test/luxc/analyser/case.lux
@@ -106,7 +106,7 @@
   (r;rec
    (function [gen-input]
      ($_ r;either
-         (r/map product;right gen-simple-primitive)
+         (r/map product;right gen-primitive)
          (do r;Monad<Random>
            [choice (|> r;nat (:: @ map (n.% (list;size variant-tags))))
             #let [choiceT (assume (list;nth choice variant-tags))
@@ -127,14 +127,14 @@
    size (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
    variant-tags (|> (r;set text;Hash<Text> size (r;text +5)) (:: @ map S;to-list))
    record-tags (|> (r;set text;Hash<Text> size (r;text +5)) (:: @ map S;to-list))
-   primitivesTC (r;list size gen-simple-primitive)
+   primitivesTC (r;list size gen-primitive)
    #let [primitivesT (L/map product;left primitivesTC)
          primitivesC (L/map product;right primitivesTC)
          variant-tags+ (L/map (|>. [module-name] code;tag) variant-tags)
          record-tags+ (L/map (|>. [module-name] code;tag) record-tags)
          variantTC (list;zip2 variant-tags+ primitivesC)]
    inputC (gen-input variant-tags+ record-tags+ primitivesC)
-   [outputT outputC] gen-simple-primitive
+   [outputT outputC] gen-primitive
    total-patterns (total-branches-for variantTC inputC)
    #let [total-branchesC (L/map (function [pattern] [pattern outputC])
                                 total-patterns)
diff --git a/new-luxc/test/test/luxc/analyser/common.lux b/new-luxc/test/test/luxc/analyser/common.lux
index 5d1dcf55e..5e8f73fd1 100644
--- a/new-luxc/test/test/luxc/analyser/common.lux
+++ b/new-luxc/test/test/luxc/analyser/common.lux
@@ -38,7 +38,7 @@
   (r;Random Code)
   (r/wrap (' [])))
 
-(def: #export gen-simple-primitive
+(def: #export gen-primitive
   (r;Random [Type Code])
   (with-expansions
     [<generators> (do-template [<type> <code-wrapper> <value-gen>]
diff --git a/new-luxc/test/test/luxc/analyser/function.lux b/new-luxc/test/test/luxc/analyser/function.lux
index fc203ca2d..fe435ebf9 100644
--- a/new-luxc/test/test/luxc/analyser/function.lux
+++ b/new-luxc/test/test/luxc/analyser/function.lux
@@ -66,8 +66,8 @@
 (test: "Function definition."
   [func-name (r;text +5)
    arg-name (|> (r;text +5) (r;filter (|>. (T/= func-name) not)))
-   [outputT outputC] gen-simple-primitive
-   [inputT _] gen-simple-primitive]
+   [outputT outputC] gen-primitive
+   [inputT _] gen-primitive]
   ($_ seq
       (assert "Can analyse function."
               (|> (&;with-expected-type (type (All [a] (-> a outputT)))
@@ -109,10 +109,10 @@
   [full-args (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
    partial-args (|> r;nat (:: @ map (n.% full-args)))
    var-idx (|> r;nat (:: @ map (|>. (n.% full-args) (n.max +1))))
-   inputsTC (r;list full-args gen-simple-primitive)
+   inputsTC (r;list full-args gen-primitive)
    #let [inputsT (L/map product;left inputsTC)
          inputsC (L/map product;right inputsTC)]
-   [outputT outputC] gen-simple-primitive
+   [outputT outputC] gen-primitive
    #let [funcT (type;function inputsT outputT)
          partialT (type;function (list;drop partial-args inputsT) outputT)
          varT (#;Bound +1)
diff --git a/new-luxc/test/test/luxc/analyser/primitive.lux b/new-luxc/test/test/luxc/analyser/primitive.lux
index 6053e2fd7..11a10088b 100644
--- a/new-luxc/test/test/luxc/analyser/primitive.lux
+++ b/new-luxc/test/test/luxc/analyser/primitive.lux
@@ -26,7 +26,7 @@
                   ["@;" common]))
   (.. common))
 
-(test: "Simple primitives"
+(test: "Primitives"
   [%bool% r;bool
    %nat% r;nat
    %int% r;int
@@ -35,27 +35,27 @@
    %char% r;char
    %text% (r;text +5)]
   (with-expansions
-    [<primitives> (do-template [<desc> <type> <tag> <value> <analyser>]
-                    [(assert (format "Can analyse " <desc> ".")
-                             (|> (@common;with-unknown-type
-                                   (<analyser> <value>))
-                                 (macro;run init-compiler)
-                                 (case> (#R;Success [_type (<tag> value)])
-                                        (and (Type/= <type> _type)
-                                             (is <value> value))
+    [<tests> (do-template [<desc> <type> <tag> <value> <analyser>]
+               [(assert (format "Can analyse " <desc> ".")
+                        (|> (@common;with-unknown-type
+                              (<analyser> <value>))
+                            (macro;run init-compiler)
+                            (case> (#R;Success [_type (<tag> value)])
+                                   (and (Type/= <type> _type)
+                                        (is <value> value))
 
-                                        _
-                                        false))
-                             )]
+                                   _
+                                   false))
+                        )]
 
-                    ["unit" Unit #~;Unit []     (function [value] @;analyse-unit)]
-                    ["bool" Bool #~;Bool %bool% @;analyse-bool]
-                    ["nat"  Nat  #~;Nat  %nat%  @;analyse-nat]
-                    ["int"  Int  #~;Int  %int%  @;analyse-int]
-                    ["deg"  Deg  #~;Deg  %deg%  @;analyse-deg]
-                    ["real" Real #~;Real %real% @;analyse-real]
-                    ["char" Char #~;Char %char% @;analyse-char]
-                    ["text" Text #~;Text %text% @;analyse-text]
-                    )]
+               ["unit" Unit #~;Unit []     (function [value] @;analyse-unit)]
+               ["bool" Bool #~;Bool %bool% @;analyse-bool]
+               ["nat"  Nat  #~;Nat  %nat%  @;analyse-nat]
+               ["int"  Int  #~;Int  %int%  @;analyse-int]
+               ["deg"  Deg  #~;Deg  %deg%  @;analyse-deg]
+               ["real" Real #~;Real %real% @;analyse-real]
+               ["char" Char #~;Char %char% @;analyse-char]
+               ["text" Text #~;Text %text% @;analyse-text]
+               )]
     ($_ seq
-        <primitives>)))
+        <tests>)))
diff --git a/new-luxc/test/test/luxc/analyser/procedure/common.lux b/new-luxc/test/test/luxc/analyser/procedure/common.lux
index 14edcf516..dc4459734 100644
--- a/new-luxc/test/test/luxc/analyser/procedure/common.lux
+++ b/new-luxc/test/test/luxc/analyser/procedure/common.lux
@@ -39,8 +39,8 @@
   )
 
 (test: "Lux procedures"
-  [[primT primC] gen-simple-primitive
-   [antiT antiC] (|> gen-simple-primitive
+  [[primT primC] gen-primitive
+   [antiT antiC] (|> gen-primitive
                      (r;filter (|>. product;left (Type/= primT) not)))]
   ($_ seq
       (assert "Can test for reference equality."
@@ -232,7 +232,7 @@
       ))
 
 (test: "Array procedures"
-  [[elemT elemC] gen-simple-primitive
+  [[elemT elemC] gen-primitive
    sizeC (|> r;nat (:: @ map code;nat))
    idxC (|> r;nat (:: @ map code;nat))
    var-name (r;text +5)
@@ -328,7 +328,7 @@
         <binary>)))
 
 (test: "Atom procedures"
-  [[elemT elemC] gen-simple-primitive
+  [[elemT elemC] gen-primitive
    sizeC (|> r;nat (:: @ map code;nat))
    idxC (|> r;nat (:: @ map code;nat))
    var-name (r;text +5)
@@ -365,7 +365,7 @@
       ))
 
 (test: "Process procedures"
-  [[primT primC] gen-simple-primitive
+  [[primT primC] gen-primitive
    timeC (|> r;nat (:: @ map code;nat))]
   ($_ seq
       (assert "Can query the level of concurrency."
diff --git a/new-luxc/test/test/luxc/analyser/reference.lux b/new-luxc/test/test/luxc/analyser/reference.lux
index 4b4355178..2acec2cad 100644
--- a/new-luxc/test/test/luxc/analyser/reference.lux
+++ b/new-luxc/test/test/luxc/analyser/reference.lux
@@ -17,7 +17,7 @@
   (.. common))
 
 (test: "References"
-  [[ref-type _] gen-simple-primitive
+  [[ref-type _] gen-primitive
    module-name (r;text +5)
    scope-name (r;text +5)
    var-name (r;text +5)]
diff --git a/new-luxc/test/test/luxc/analyser/structure.lux b/new-luxc/test/test/luxc/analyser/structure.lux
index 2b75baa9a..801f61616 100644
--- a/new-luxc/test/test/luxc/analyser/structure.lux
+++ b/new-luxc/test/test/luxc/analyser/structure.lux
@@ -57,9 +57,9 @@
 (test: "Sums"
   [size (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
    choice (|> r;nat (:: @ map (n.% size)))
-   primitives (r;list size gen-simple-primitive)
+   primitives (r;list size gen-primitive)
    +choice (|> r;nat (:: @ map (n.% (n.inc size))))
-   [_ +valueC] gen-simple-primitive
+   [_ +valueC] gen-primitive
    #let [variantT (type;variant (L/map product;left primitives))
          [valueT valueC] (assume (list;nth choice primitives))
          +size (n.inc size)
@@ -136,9 +136,9 @@
 
 (test: "Products"
   [size (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
-   primitives (r;list size gen-simple-primitive)
+   primitives (r;list size gen-primitive)
    choice (|> r;nat (:: @ map (n.% size)))
-   [_ +valueC] gen-simple-primitive
+   [_ +valueC] gen-primitive
    #let [[singletonT singletonC] (|> primitives (list;nth choice) assume)
          +primitives (list;concat (list (list;take choice primitives)
                                         (list [(#;Bound +1) +valueC])
@@ -243,7 +243,7 @@
    tags (|> (r;set text;Hash<Text> size (r;text +5)) (:: @ map S;to-list))
    choice (|> r;nat (:: @ map (n.% size)))
    other-choice (|> r;nat (:: @ map (n.% size)) (r;filter (|>. (n.= choice) not)))
-   primitives (r;list size gen-simple-primitive)
+   primitives (r;list size gen-primitive)
    module-name (r;text +5)
    type-name (r;text +5)
    #let [varT (#;Bound +1)
@@ -305,7 +305,7 @@
 (test: "Records"
   [size (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
    tags (|> (r;set text;Hash<Text> size (r;text +5)) (:: @ map S;to-list))
-   primitives (r;list size gen-simple-primitive)
+   primitives (r;list size gen-primitive)
    module-name (r;text +5)
    type-name (r;text +5)
    choice (|> r;nat (:: @ map (n.% size)))
diff --git a/new-luxc/test/test/luxc/synthesizer/common.lux b/new-luxc/test/test/luxc/synthesizer/common.lux
new file mode 100644
index 000000000..c02e23c7c
--- /dev/null
+++ b/new-luxc/test/test/luxc/synthesizer/common.lux
@@ -0,0 +1,37 @@
+(;module:
+  lux
+  (lux (data [bool "B/" Eq<Bool>]
+             [char "C/" Eq<Char>]
+             [text "T/" Eq<Text>])
+       ["r" math/random "r/" Monad<Random>])
+  (luxc (lang ["la" analysis]
+              ["ls" synthesis])))
+
+(def: #export gen-primitive
+  (r;Random la;Analysis)
+  (r;either (r;either (r;either (r/wrap #la;Unit)
+                                (r/map (|>. #la;Bool) r;bool))
+                      (r;either (r/map (|>. #la;Nat) r;nat)
+                                (r/map (|>. #la;Int) r;int)))
+            (r;either (r;either (r/map (|>. #la;Deg) r;deg)
+                                (r/map (|>. #la;Real) r;real))
+                      (r;either (r/map (|>. #la;Char) r;char)
+                                (r/map (|>. #la;Text) (r;text +5))))))
+
+(def: #export (corresponds? analysis synthesis)
+  (-> la;Analysis ls;Synthesis Bool)
+  (case [analysis synthesis]
+    (^template [<analysis> <synthesis> <test>]
+      [(<analysis> valueA) (<synthesis> valueS)]
+      (<test> valueA valueS))
+    ([#la;Unit #ls;Unit is]
+     [#la;Bool #ls;Bool B/=]
+     [#la;Nat  #ls;Nat  n.=]
+     [#la;Int  #ls;Int  i.=]
+     [#la;Deg  #ls;Deg  d.=]
+     [#la;Real #ls;Real r.=]
+     [#la;Char #ls;Char C/=]
+     [#la;Text #ls;Text T/=])
+
+    _
+    false))
diff --git a/new-luxc/test/test/luxc/synthesizer/function.lux b/new-luxc/test/test/luxc/synthesizer/function.lux
new file mode 100644
index 000000000..9243294a2
--- /dev/null
+++ b/new-luxc/test/test/luxc/synthesizer/function.lux
@@ -0,0 +1,33 @@
+(;module:
+  lux
+  (lux [io]
+       (control monad
+                pipe)
+       (data [product]
+             (coll [list]))
+       ["r" math/random "r/" Monad<Random>]
+       test)
+  (luxc (lang ["la" analysis]
+              ["ls" synthesis])
+        (analyser [";A" structure])
+        [synthesizer])
+  (.. common))
+
+(test: "Function application."
+  [num-args (|> r;nat (:: @ map (|>. (n.% +10) (n.max +1))))
+   funcA gen-primitive
+   argsA (r;list num-args gen-primitive)]
+  ($_ seq
+      (assert "Can synthesize function application."
+              (|> (synthesizer;synthesize (la;apply argsA funcA))
+                  (case> (#ls;Call funcS argsS)
+                         (and (corresponds? funcA funcS)
+                              (list;every? (product;uncurry corresponds?)
+                                           (list;zip2 argsA argsS)))
+                         
+                         _
+                         false)))
+      (assert "Function application on no arguments just synthesizes to the function itself."
+              (|> (synthesizer;synthesize (la;apply (list) funcA))
+                  (corresponds? funcA)))
+      ))
diff --git a/new-luxc/test/test/luxc/synthesizer/primitive.lux b/new-luxc/test/test/luxc/synthesizer/primitive.lux
new file mode 100644
index 000000000..4c67fa0a4
--- /dev/null
+++ b/new-luxc/test/test/luxc/synthesizer/primitive.lux
@@ -0,0 +1,41 @@
+(;module:
+  lux
+  (lux [io]
+       (control monad
+                pipe)
+       (data text/format)
+       ["r" math/random "R/" Monad<Random>]
+       test)
+  (luxc (lang ["la" analysis]
+              ["ls" synthesis])
+        [analyser]
+        [synthesizer]))
+
+(test: "Primitives"
+  [%bool% r;bool
+   %nat% r;nat
+   %int% r;int
+   %deg% r;deg
+   %real% r;real
+   %char% r;char
+   %text% (r;text +5)]
+  (with-expansions
+    [<tests> (do-template [<desc> <analysis> <synthesis> <sample>]
+               [(assert (format "Can synthesize " <desc> ".")
+                        (|> (synthesizer;synthesize (<analysis> <sample>))
+                            (case> (<synthesis> value)
+                                   (is <sample> value)
+
+                                   _
+                                   false)))]
+
+               ["unit" #la;Unit #ls;Unit []]
+               ["bool" #la;Bool #ls;Bool %bool%]
+               ["nat"  #la;Nat  #ls;Nat  %nat%]
+               ["int"  #la;Int  #ls;Int  %int%]
+               ["deg"  #la;Deg  #ls;Deg  %deg%]
+               ["real" #la;Real #ls;Real %real%]
+               ["char" #la;Char #ls;Char %char%]
+               ["text" #la;Text #ls;Text %text%])]
+    ($_ seq
+        <tests>)))
diff --git a/new-luxc/test/test/luxc/synthesizer/procedure.lux b/new-luxc/test/test/luxc/synthesizer/procedure.lux
new file mode 100644
index 000000000..898987308
--- /dev/null
+++ b/new-luxc/test/test/luxc/synthesizer/procedure.lux
@@ -0,0 +1,32 @@
+(;module:
+  lux
+  (lux [io]
+       (control monad
+                pipe)
+       (data [bool "B/" Eq<Bool>]
+             [text "T/" Eq<Text>]
+             [product]
+             (coll [list]))
+       ["r" math/random "r/" Monad<Random>]
+       test)
+  (luxc (lang ["la" analysis]
+              ["ls" synthesis])
+        (analyser [";A" structure])
+        [synthesizer])
+  (.. common))
+
+(test: "Procedures"
+  [num-args (|> r;nat (:: @ map (n.% +10)))
+   nameA (r;text +5)
+   argsA (r;list num-args gen-primitive)]
+  ($_ seq
+      (assert "Can synthesize procedure calls."
+              (|> (synthesizer;synthesize (#la;Procedure nameA argsA))
+                  (case> (#ls;Procedure nameS argsS)
+                         (and (T/= nameA nameS)
+                              (list;every? (product;uncurry corresponds?)
+                                           (list;zip2 argsA argsS)))
+                         
+                         _
+                         false)))
+      ))
diff --git a/new-luxc/test/test/luxc/synthesizer/structure.lux b/new-luxc/test/test/luxc/synthesizer/structure.lux
new file mode 100644
index 000000000..3f90bf321
--- /dev/null
+++ b/new-luxc/test/test/luxc/synthesizer/structure.lux
@@ -0,0 +1,45 @@
+(;module:
+  lux
+  (lux [io]
+       (control monad
+                pipe)
+       (data [bool "B/" Eq<Bool>]
+             [product]
+             (coll [list]))
+       ["r" math/random "r/" Monad<Random>]
+       test)
+  (luxc (lang ["la" analysis]
+              ["ls" synthesis])
+        [synthesizer])
+  (.. common))
+
+(test: "Variants"
+  [size (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
+   tagA (|> r;nat (:: @ map (n.% size)))
+   memberA gen-primitive]
+  ($_ seq
+      (assert "Can synthesize variants."
+              (|> (synthesizer;synthesize (la;sum tagA size +0 memberA))
+                  (case> (#ls;Variant tagS last?S memberS)
+                         (and (n.= tagA tagS)
+                              (B/= (n.= (n.dec size) tagA)
+                                   last?S)
+                              (corresponds? memberA memberS))
+                         
+                         _
+                         false)))
+      ))
+
+(test: "Tuples"
+  [size (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
+   membersA (r;list size gen-primitive)]
+  ($_ seq
+      (assert "Can synthesize tuple."
+              (|> (synthesizer;synthesize (la;product membersA))
+                  (case> (#ls;Tuple membersS)
+                         (and (n.= size (list;size membersS))
+                              (list;every? (product;uncurry corresponds?) (list;zip2 membersA membersS)))
+
+                         _
+                         false)))
+      ))
diff --git a/new-luxc/test/tests.lux b/new-luxc/test/tests.lux
index 26ec28743..114768c2d 100644
--- a/new-luxc/test/tests.lux
+++ b/new-luxc/test/tests.lux
@@ -5,14 +5,17 @@
        (concurrency [promise])
        [cli #+ program:]
        [test])
-  (test (luxc ["_;" parser]
-              (analyser ["_;" primitive]
-                        ["_;" structure]
-                        ["_;" reference]
-                        ["_;" case]
-                        ["_;" function]
-                        (procedure ["_;" common])
-                        ))))
+  (test (luxc ["_;P" parser]
+              (analyser ["_;A" primitive]
+                        ["_;A" structure]
+                        ["_;A" reference]
+                        ["_;A" case]
+                        ["_;A" function]
+                        (procedure ["_;A" common]))
+              (synthesizer ["_;S" primitive]
+                           ["_;S" structure]
+                           ["_;S" function]
+                           ["_;S" procedure]))))
 
 ## [Program]
 (program: args