aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2017-05-31 21:35:39 -0400
committerEduardo Julian2017-05-31 21:35:39 -0400
commitaa3dcb411db1bfbf41ca59c334c6c792b9e40d0c (patch)
tree0095015807b18d65e9938cf9db686d8f29d87afb
parentb73f1c909d19d5492d6d9a7dc707a3b817c73619 (diff)
- Implemented some synthesis algorithms and tests for primitives, structures, procedures and function application.
- Some refactoring.
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/analyser/function.lux5
-rw-r--r--new-luxc/source/luxc/analyser/structure.lux55
-rw-r--r--new-luxc/source/luxc/lang/analysis.lux61
-rw-r--r--new-luxc/source/luxc/lang/synthesis.lux30
-rw-r--r--new-luxc/source/luxc/synthesizer.lux278
-rw-r--r--new-luxc/test/test/luxc/analyser/case.lux6
-rw-r--r--new-luxc/test/test/luxc/analyser/common.lux2
-rw-r--r--new-luxc/test/test/luxc/analyser/function.lux8
-rw-r--r--new-luxc/test/test/luxc/analyser/primitive.lux44
-rw-r--r--new-luxc/test/test/luxc/analyser/procedure/common.lux10
-rw-r--r--new-luxc/test/test/luxc/analyser/reference.lux2
-rw-r--r--new-luxc/test/test/luxc/analyser/structure.lux12
-rw-r--r--new-luxc/test/test/luxc/synthesizer/common.lux37
-rw-r--r--new-luxc/test/test/luxc/synthesizer/function.lux33
-rw-r--r--new-luxc/test/test/luxc/synthesizer/primitive.lux41
-rw-r--r--new-luxc/test/test/luxc/synthesizer/procedure.lux32
-rw-r--r--new-luxc/test/test/luxc/synthesizer/structure.lux45
-rw-r--r--new-luxc/test/tests.lux19
18 files changed, 569 insertions, 151 deletions
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 1aad8954e..5144534fb 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -100,7 +100,4 @@
[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)))))
+ (wrap (la;apply argsA funcA)))))
diff --git a/new-luxc/source/luxc/analyser/structure.lux b/new-luxc/source/luxc/analyser/structure.lux
index f93534463..37266b2fe 100644
--- a/new-luxc/source/luxc/analyser/structure.lux
+++ b/new-luxc/source/luxc/analyser/structure.lux
@@ -24,37 +24,6 @@
(analyser ["&;" common]
["&;" inference])))
-## Variants get analysed as binary sum types for the sake of semantic
-## simplicity.
-## This is because you can encode a variant of any size using just
-## binary sums by nesting them.
-
-(do-template [<name> <side>]
- [(def: (<name> inner)
- (-> la;Analysis la;Analysis)
- (#la;Sum (<side> inner)))]
-
- [sum-left #;Left]
- [sum-right #;Right])
-
-(def: (variant tag size temp value)
- (-> Nat Nat Nat la;Analysis la;Analysis)
- (if (n.= (n.dec size) tag)
- (if (n.= +1 tag)
- (sum-right value)
- (L/fold (function;const sum-left)
- (sum-right value)
- (list;n.range +0 (n.- +2 tag))))
- (L/fold (function;const sum-left)
- (case value
- (#la;Sum _)
- (#la;Case value (list [(#la;BindP temp)
- (#la;Relative (#;Local temp))]))
-
- _
- value)
- (list;n.range +0 tag))))
-
(def: #export (analyse-sum analyse tag valueC)
(-> &;Analyser Nat Code (Lux la;Analysis))
(do Monad<Lux>
@@ -71,7 +40,7 @@
[valueA (&;with-expected-type variant-type
(analyse valueC))
temp &env;next-local]
- (wrap (variant tag type-size temp valueA)))
+ (wrap (la;sum tag type-size temp valueA)))
#;None
(&common;variant-out-of-bounds-error expected type-size tag)))
@@ -111,22 +80,6 @@
_
(&;fail "")))))
-## Tuples get analysed into binary products for the sake of semantic
-## simplicity, since products/pairs can encode tuples of any length
-## through nesting.
-
-(def: (product members)
- (-> (List la;Analysis) la;Analysis)
- (case members
- #;Nil
- #la;Unit
-
- (#;Cons singleton #;Nil)
- singleton
-
- (#;Cons left right)
- (#la;Product left (product right))))
-
(def: (analyse-typed-product analyse members)
(-> &;Analyser (List Code) (Lux la;Analysis))
(do Monad<Lux>
@@ -206,7 +159,7 @@
_ (&;within-type-env
(TC;check expected
(type;tuple (L/map product;left membersTA))))]
- (wrap (product (L/map product;right membersTA))))))
+ (wrap (la;product (L/map product;right membersTA))))))
(#;UnivQ _)
(do @
@@ -237,7 +190,7 @@
_ (&;within-type-env
(TC;check expectedT inferredT))
temp &env;next-local]
- (wrap (variant idx case-size temp (|> valueA+ list;head assume)))))
+ (wrap (la;sum idx case-size temp (|> valueA+ list;head assume)))))
## There cannot be any ambiguity or improper syntax when analysing
## records, so they must be normalized for further analysis.
@@ -312,4 +265,4 @@
[inferredT membersA] (&inference;apply-function analyse inferenceT members)
_ (&;within-type-env
(TC;check expectedT inferredT))]
- (wrap (product membersA))))
+ (wrap (la;product membersA))))
diff --git a/new-luxc/source/luxc/lang/analysis.lux b/new-luxc/source/luxc/lang/analysis.lux
index b96bd9ba2..2e122a526 100644
--- a/new-luxc/source/luxc/lang/analysis.lux
+++ b/new-luxc/source/luxc/lang/analysis.lux
@@ -1,5 +1,7 @@
(;module:
- lux)
+ lux
+ (lux [function]
+ (data (coll [list "L/" Fold<List>]))))
(type: #export #rec Pattern
(#BindP Nat)
@@ -30,3 +32,60 @@
(#Procedure Text (List Analysis))
(#Relative Ref)
(#Absolute Ident))
+
+## Variants get analysed as binary sum types for the sake of semantic
+## simplicity.
+## This is because you can encode a variant of any size using just
+## binary sums by nesting them.
+
+(do-template [<name> <side>]
+ [(def: (<name> inner)
+ (-> Analysis Analysis)
+ (#Sum (<side> inner)))]
+
+ [sum-left #;Left]
+ [sum-right #;Right])
+
+(def: #export (sum tag size temp value)
+ (-> Nat Nat Nat Analysis Analysis)
+ (if (n.= (n.dec size) tag)
+ (if (n.= +1 tag)
+ (sum-right value)
+ (L/fold (function;const sum-left)
+ (sum-right value)
+ (list;n.range +0 (n.- +2 tag))))
+ (L/fold (function;const sum-left)
+ (case value
+ (#Sum _)
+ (#Case value (list [(#BindP temp)
+ (#Relative (#;Local temp))]))
+
+ _
+ value)
+ (list;n.range +0 tag))))
+
+## Tuples get analysed into binary products for the sake of semantic
+## simplicity, since products/pairs can encode tuples of any length
+## through nesting.
+
+(def: #export (product members)
+ (-> (List Analysis) Analysis)
+ (case members
+ #;Nil
+ #Unit
+
+ (#;Cons singleton #;Nil)
+ singleton
+
+ (#;Cons left right)
+ (#Product left (product right))))
+
+## Function application gets analysed into single-argument
+## applications, since every other kind of application can be encoded
+## into a finite series of single-argument applications.
+
+(def: #export (apply args func)
+ (-> (List Analysis) Analysis Analysis)
+ (L/fold (function [arg func] (#Apply arg func))
+ func
+ args))
diff --git a/new-luxc/source/luxc/lang/synthesis.lux b/new-luxc/source/luxc/lang/synthesis.lux
index 491891600..5fd6a3a81 100644
--- a/new-luxc/source/luxc/lang/synthesis.lux
+++ b/new-luxc/source/luxc/lang/synthesis.lux
@@ -1,6 +1,21 @@
(;module:
- lux
- (.. ["lp" pattern]))
+ lux)
+
+(type: #export (Path' s)
+ #PopP
+ (#BindP Nat)
+ (#BoolP Bool)
+ (#NatP Nat)
+ (#IntP Int)
+ (#DegP Deg)
+ (#RealP Real)
+ (#CharP Char)
+ (#TextP Text)
+ (#VariantP (Either Nat Nat))
+ (#TupleP (Either Nat Nat))
+ (#AltP (Path' s) (Path' s))
+ (#SeqP (Path' s) (Path' s))
+ (#ExecP s))
(type: #export #rec Synthesis
#Unit
@@ -13,10 +28,15 @@
(#Text Text)
(#Variant Nat Bool Synthesis)
(#Tuple (List Synthesis))
- (#Case (List [lp;Pattern Synthesis]))
+ (#Case Synthesis (Path' Synthesis))
(#Function Nat Scope Synthesis)
(#Call Synthesis (List Synthesis))
(#Recur Nat (List Synthesis))
(#Procedure Text (List Synthesis))
- (#Relative Ref)
- (#Absolute Ident))
+ (#Relative Int)
+ (#Absolute Ident)
+ (#Let Nat Synthesis Synthesis)
+ (#If Synthesis Synthesis Synthesis)
+ (#Loop Nat (List Synthesis) Synthesis))
+
+(type: #export Path (Path' Synthesis))
diff --git a/new-luxc/source/luxc/synthesizer.lux b/new-luxc/source/luxc/synthesizer.lux
index 6acd2a0a2..04a699993 100644
--- a/new-luxc/source/luxc/synthesizer.lux
+++ b/new-luxc/source/luxc/synthesizer.lux
@@ -1,45 +1,243 @@
(;module:
lux
- (lux (control monad)
- (data text/format
- (coll [list "L/" Functor<List>]))
- [macro #+ Monad<Lux>])
+ (lux (data (coll [list "L/" Functor<List>])))
(luxc ["&" base]
- (lang ["la" analysis #+ Analysis]
- ["ls" synthesis #+ Synthesis])
- ["&;" analyser]))
+ (lang ["la" analysis]
+ ["ls" synthesis])
+ ## (synthesizer ["&&;" case])
+ ))
+
+## (do-template [<name> <comp>]
+## [(def: (<name> ref)
+## (-> Int Bool)
+## (<comp> 0 ref))]
+
+## [function-ref? i.=]
+## [local-ref? i.>]
+## [captured-ref? i.<]
+## )
+
+(def: (unfold-tuple tuple)
+ (-> la;Analysis (List la;Analysis))
+ (case tuple
+ (#la;Product left right)
+ (#;Cons left (unfold-tuple right))
+
+ _
+ (list tuple)))
+
+(def: (unfold-apply apply)
+ (-> la;Analysis [la;Analysis (List la;Analysis)])
+ (loop [apply apply
+ args (list)]
+ (case apply
+ (#la;Apply arg func)
+ (recur func (#;Cons arg args))
+
+ _
+ [apply args])))
+
+(def: (unfold-variant variant)
+ (-> (Either la;Analysis la;Analysis) [Nat Bool la;Analysis])
+ (loop [so-far +0
+ variantA variant]
+ (case variantA
+ (#;Left valueA)
+ (case valueA
+ (#la;Sum choice)
+ (recur (n.inc so-far) choice)
+
+ _
+ [so-far false valueA])
+
+ (#;Right valueA)
+ [(n.inc so-far) true valueA])))
+
+## (def: (has-self-reference? exprS)
+## (-> ls;Synthesis Bool)
+## (case exprS
+## (#ls;Tuple membersS)
+## (list;any? has-self-reference? membersS)
+
+## (#ls;Procedure name argsS)
+## (list;any? has-self-reference? argsS)
+
+## (#ls;Variant tag last? memberS)
+## (has-self-reference? memberS)
+
+## (#ls;Relative idx)
+## (i.= 0 idx)
+
+## (#ls;Recur offset argsS)
+## (list;any? has-self-reference? argsS)
+
+## (#ls;Call funcS argsS)
+## (or (has-self-reference? funcS)
+## (list;any? has-self-reference? argsS))
+
+## (#ls;Let register inputS bodyS)
+## (or (has-self-reference? inputS)
+## (has-self-reference? bodyS))
+
+## (#ls;If inputS thenS elseS)
+## (or (has-self-reference? inputS)
+## (has-self-reference? thenS)
+## (has-self-reference? elseS))
+
+## (#ls;Function num-args scope bodyS)
+## (not (list;any? (i.= 0) scope))
+
+## (#ls;Loop offset argsS bodyS)
+## (or (list;any? has-self-reference? argsS)
+## (has-self-reference? bodyS))
+
+## _
+## false
+## ))
+
+## (def: (shift-loop-variables scope offset exprS)
+## (-> (List Int) Nat ls;Synthesis ls;Synthesis)
+## (loop [exprS exprS]
+## (case exprS
+## (#ls;Tuple members)
+## (#ls;Tuple (L/map recur members))
+
+## (#ls;Procedure name argsS)
+## (#ls;Procedure name (L/map recur argsS))
+
+## (#ls;Variant tag last? valueS)
+## (#ls;Variant tag last? (recur valueS))
+
+## (#ls;Relative idx)
+## (if (captured-ref? idx)
+## (let [scope-idx (|> idx (n.+ 1) (n.* -1) int-to-nat)]
+## (|> scope (list;nth scope-idx) assume #ls;Relative))
+## (#ls;Relative (i.+ idx (nat-to-int offset))))
+
+## (#ls;Recur _offset argsS)
+## (#ls;Recur (n.+ offset _offset) (L/map recur argsS))
+
+## (#ls;Call funcS argsS)
+## (#ls;Call (recur funcS) (L/map recur argsS))
+
+## (#ls;Let register inputS bodyS)
+## (#ls;Let (n.+ offset register) (recur inputS) (recur bodyS))
+
+## (#ls;If inputS thenS elseS)
+## (#ls;If (recur inputS) (recur thenS) (recur elseS))
+
+## (#ls;Function _num-args _scope _bodyS)
+## ...
+
+## (#ls;Loop _offset _argsS _bodyS)
+## (#ls;Loop (n.+ offset _offset) (L/map recur _argsS) (recur _bodyS))
+
+## _
+## exprS
+## )))
(def: #export (synthesize analysis)
- (-> Analysis Synthesis)
- (case analysis
- (^template [<from> <to>]
- (<from> value)
- (<to> value))
- ([#la;Bool #ls;Bool]
- [#la;Nat #ls;Nat]
- [#la;Int #ls;Int]
- [#la;Deg #ls;Deg]
- [#la;Real #ls;Real]
- [#la;Char #ls;Char]
- [#la;Text #ls;Text]
- [#la;Relative #ls;Relative]
- [#la;Absolute #ls;Absolute])
-
- (#la;Tuple values)
- (#ls;Tuple (L/map synthesize values))
-
- (#la;Variant tag last? value)
- (undefined)
-
- (#la;Case input matches)
- (undefined)
-
- (#la;Function scope body)
- (undefined)
-
- (#la;Apply arg func)
- (undefined)
-
- (#la;Procedure name args)
- (#ls;Procedure name (L/map synthesize args))
- ))
+ (-> la;Analysis ls;Synthesis)
+ (loop [num-args +0
+ local-offset +0
+ tail? true
+ exprA analysis]
+ (case exprA
+ (^template [<from> <to>]
+ (<from> value)
+ (<to> value))
+ ([#la;Unit #ls;Unit]
+ [#la;Bool #ls;Bool]
+ [#la;Nat #ls;Nat]
+ [#la;Int #ls;Int]
+ [#la;Deg #ls;Deg]
+ [#la;Real #ls;Real]
+ [#la;Char #ls;Char]
+ [#la;Text #ls;Text]
+ [#la;Absolute #ls;Absolute])
+
+ (#la;Product _)
+ (#ls;Tuple (L/map (recur +0 local-offset false) (unfold-tuple exprA)))
+
+ (#la;Sum choice)
+ (let [[tag last? value] (unfold-variant choice)]
+ (#ls;Variant tag last? (recur +0 local-offset false value)))
+
+ (#la;Apply _)
+ (let [[funcA argsA] (unfold-apply exprA)
+ funcS (recur +0 local-offset false funcA)
+ argsS (L/map (recur +0 local-offset false) argsA)]
+ (case funcS
+ ## (^multi (#ls;Relative idx)
+ ## (and (|> num-args n.dec nat-to-int (i.* -1) (i.= idx))
+ ## tail?))
+ ## (#ls;Recur +1 argsS)
+
+ ## (^multi (#ls;Function _num-args _scope _bodyS)
+ ## (and (n.= _num-args (list;size argsS))
+ ## (not (has-self-reference? _bodyS))))
+ ## (#ls;Loop local-offset argsS (shift-loop-variables local-offset _bodyS))
+
+ _
+ (#ls;Call funcS argsS)))
+
+ (#la;Procedure name args)
+ (#ls;Procedure name (L/map (recur +0 local-offset false) args))
+
+ _
+ (undefined)
+
+ ## (#la;Relative ref)
+ ## (case ref
+ ## (#;Local local)
+ ## (case local
+ ## +0
+ ## (if (n.> +1 num-args)
+ ## (<| (#ls;Call (#ls;Relative 0))
+ ## (L/map (|>. #ls;Relative))
+ ## (list;range +1 (n.dec num-args)))
+ ## (#ls;Relative 0))
+
+ ## _
+ ## (#ls;Relative (nat-to-int (n.+ (n.inc num-args) local))))
+
+ ## (#;Captured captured)
+ ## (#ls;Relative (|> captured nat-to-int (n.* -1) (n.+ -1))))
+
+ ## (#la;Function scope bodyA)
+ ## (case (recur (n.inc num-args) local-offset true bodyA)
+ ## (#ls;Function num-args' scope' bodyS')
+ ## (#ls;Function (n.inc num-args') scope bodyS')
+
+ ## bodyS
+ ## (#ls;Function +1 scope bodyS))
+
+ ## (#la;Case inputA branchesA)
+ ## (let [inputS (recur num-args local-offset false inputA)]
+ ## (case branchesA
+ ## (^multi (^ (list [(#lp;Bind input-register)
+ ## (#la;Relative (#;Local output-register))]))
+ ## (n.= input-register output-register))
+ ## inputS
+
+ ## (^ (list [(#lp;Bind register) bodyA]))
+ ## (#ls;Let register inputS (recur num-args local-offset tail? bodyA))
+
+ ## (^or (^ (list [(#lp;Bool true) thenA] [(#lp;Bool false) elseA]))
+ ## (^ (list [(#lp;Bool false) elseA] [(#lp;Bool true) thenA])))
+ ## (#ls;If inputS
+ ## (recur num-args local-offset tail? thenA)
+ ## (recur num-args local-offset tail? elseA))
+
+ ## (#;Cons [headP headA] tailPA)
+ ## (let [headP+ (|> (recur num-args local-offset tail? headA)
+ ## #ls;ExecP
+ ## (#ls;SeqP (&&case;path headP)))
+ ## tailP+ (L/map (function [[pattern bodyA]]
+ ## (|> (recur num-args local-offset tail? bodyA)
+ ## #ls;ExecP
+ ## (#ls;SeqP (&&case;path pattern))))
+ ## tailPA)]
+ ## (#ls;Case inputS (&&case;weave-paths headP+ tailP+)))
+ ## ))
+ )))
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