From aa3dcb411db1bfbf41ca59c334c6c792b9e40d0c Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 31 May 2017 21:35:39 -0400 Subject: - Implemented some synthesis algorithms and tests for primitives, structures, procedures and function application. - Some refactoring. --- new-luxc/source/luxc/analyser/function.lux | 5 +- new-luxc/source/luxc/analyser/structure.lux | 55 +----- new-luxc/source/luxc/lang/analysis.lux | 61 +++++- new-luxc/source/luxc/lang/synthesis.lux | 30 ++- new-luxc/source/luxc/synthesizer.lux | 278 ++++++++++++++++++++++++---- 5 files changed, 328 insertions(+), 101 deletions(-) (limited to 'new-luxc/source') 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 [ ] - [(def: ( inner) - (-> la;Analysis la;Analysis) - (#la;Sum ( 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 @@ -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 @@ -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])))) (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 [ ] + [(def: ( inner) + (-> Analysis Analysis) + (#Sum ( 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])) - [macro #+ Monad]) + (lux (data (coll [list "L/" Functor]))) (luxc ["&" base] - (lang ["la" analysis #+ Analysis] - ["ls" synthesis #+ Synthesis]) - ["&;" analyser])) + (lang ["la" analysis] + ["ls" synthesis]) + ## (synthesizer ["&&;" case]) + )) + +## (do-template [ ] +## [(def: ( ref) +## (-> Int Bool) +## ( 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 [ ] - ( value) - ( 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 [ ] + ( value) + ( 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+))) + ## )) + ))) -- cgit v1.2.3