diff options
Diffstat (limited to '')
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 |