From c50667a431a5ca67328a230f0c59956dc6ff43fa Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Fri, 9 Jun 2017 20:53:26 -0400 Subject: - Added loop synthesis. - Some refactoring. --- new-luxc/source/luxc/analyser/case/coverage.lux | 8 +- new-luxc/source/luxc/lang/synthesis.lux | 10 +- new-luxc/source/luxc/synthesizer.lux | 171 +++++++---------------- new-luxc/source/luxc/synthesizer/function.lux | 23 +-- new-luxc/source/luxc/synthesizer/loop.lux | 166 ++++++++++++++++++++++ new-luxc/test/test/luxc/synthesizer/function.lux | 3 +- new-luxc/test/test/luxc/synthesizer/loop.lux | 164 ++++++++++++++++++++++ new-luxc/test/tests.lux | 3 +- 8 files changed, 404 insertions(+), 144 deletions(-) create mode 100644 new-luxc/source/luxc/synthesizer/loop.lux create mode 100644 new-luxc/test/test/luxc/synthesizer/loop.lux diff --git a/new-luxc/source/luxc/analyser/case/coverage.lux b/new-luxc/source/luxc/analyser/case/coverage.lux index 754e555b2..5989952ee 100644 --- a/new-luxc/source/luxc/analyser/case/coverage.lux +++ b/new-luxc/source/luxc/analyser/case/coverage.lux @@ -271,13 +271,13 @@ #;None (case (list;reverse possibilities) - #;Nil - (R;fail "{ This is not supposed to happen... }") - (#;Cons last prevs) (wrap (L/fold (function [left right] (#Alt left right)) last - prevs)))))) + prevs)) + + #;Nil + (undefined))))) _ (if (C/= so-far addition) diff --git a/new-luxc/source/luxc/lang/synthesis.lux b/new-luxc/source/luxc/lang/synthesis.lux index f5d3f9c33..b86f49fb2 100644 --- a/new-luxc/source/luxc/lang/synthesis.lux +++ b/new-luxc/source/luxc/lang/synthesis.lux @@ -1,6 +1,8 @@ (;module: lux) +(def: #export Arity Nat) +(def: #export Register Nat) (def: #export Variable Int) (type: #export (Path' s) @@ -31,14 +33,14 @@ (#Variant Nat Bool Synthesis) (#Tuple (List Synthesis)) (#Case Synthesis (Path' Synthesis)) - (#Function Nat (List Variable) Synthesis) + (#Function Arity (List Variable) Synthesis) (#Call Synthesis (List Synthesis)) - (#Recur Nat (List Synthesis)) + (#Recur (List Synthesis)) (#Procedure Text (List Synthesis)) (#Variable Variable) (#Definition Ident) - (#Let Nat Synthesis Synthesis) + (#Let Register Synthesis Synthesis) (#If Synthesis Synthesis Synthesis) - (#Loop Nat (List Synthesis) Synthesis)) + (#Loop Register (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 5dc4fa258..2f7344c6e 100644 --- a/new-luxc/source/luxc/synthesizer.lux +++ b/new-luxc/source/luxc/synthesizer.lux @@ -2,105 +2,30 @@ lux (lux (data text/format [number] - (coll [list "L/" Functor Fold] + (coll [list "L/" Functor Fold Monoid] ["d" dict]))) (luxc ["&" base] (lang ["la" analysis] ["ls" synthesis]) (synthesizer ["&&;" structure] - ["&&;" function]) + ["&&;" function] + ["&&;" loop]) )) -## (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;Variable 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;Variable idx) -## (if (captured-ref? idx) -## (let [scope-idx (|> idx (n.+ 1) (n.* -1) int-to-nat)] -## (|> scope (list;nth scope-idx) assume #ls;Variable)) -## (#ls;Variable (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: init-env (List ls;Variable) (list)) (def: init-resolver (d;Dict Int Int) (d;new number;Hash)) +(def: (prepare-body inner-arity arity body) + (-> Nat Nat ls;Synthesis ls;Synthesis) + (if (&&function;nested? inner-arity) + body + (&&loop;reify-recursion arity body))) + (def: #export (synthesize analysis) (-> la;Analysis ls;Synthesis) - (loop [scope-args +0 + (loop [outer-arity +0 resolver init-resolver + num-locals +0 exprA analysis] (case exprA (^template [ ] @@ -117,34 +42,29 @@ [#la;Absolute #ls;Definition]) (#la;Product _) - (#ls;Tuple (L/map (recur +0 resolver) (&&structure;unfold-tuple exprA))) + (#ls;Tuple (L/map (recur +0 resolver num-locals) (&&structure;unfold-tuple exprA))) (#la;Sum choice) (let [[tag last? value] (&&structure;unfold-variant choice)] - (#ls;Variant tag last? (recur +0 resolver value))) + (#ls;Variant tag last? (recur +0 resolver num-locals value))) (#la;Relative ref) - (if (&&function;nested-function? scope-args) - (case ref - (#;Local local) - (if (n.= +0 local) + (case ref + (#;Local register) + (if (&&function;nested? outer-arity) + (if (n.= +0 register) (<| (#ls;Call (#ls;Variable 0)) - (L/map (|>. nat-to-int #ls;Variable)) - (list;n.range +1 (n.dec scope-args))) - (#ls;Variable (&&function;adjust-var scope-args (nat-to-int local)))) - - (#;Captured register) - (#ls;Variable (default (&&function;to-captured register) - (d;get (&&function;to-captured register) resolver)))) - (case ref - (#;Local local) - (#ls;Variable (nat-to-int local)) - - (#;Captured register) - (#ls;Variable (&&function;to-captured register)))) + (L/map (|>. &&function;to-local #ls;Variable)) + (list;n.range +1 (n.dec outer-arity))) + (#ls;Variable (&&function;adjust-var outer-arity (&&function;to-local register)))) + (#ls;Variable (&&function;to-local register))) + + (#;Captured register) + (#ls;Variable (let [var (&&function;to-captured register)] + (default var (d;get var resolver))))) (#la;Function scope bodyA) - (let [num-args (n.inc scope-args) + (let [inner-arity (n.inc outer-arity) raw-env (&&function;environment scope) env (L/map (function [var] (default var (d;get var resolver))) raw-env) env-vars (let [env-size (list;size raw-env)] @@ -152,7 +72,7 @@ (case env-size +0 (list) _ (L/map &&function;to-captured (list;n.range +0 (n.dec env-size)))))) - resolver' (if (&&function;nested-function? num-args) + resolver' (if (&&function;nested? inner-arity) (L/fold (function [[from to] resolver'] (d;put from to resolver')) init-resolver @@ -161,33 +81,36 @@ (d;put var var resolver')) init-resolver env-vars))] - (case (recur num-args resolver' bodyA) - (#ls;Function args' env' bodyS') - (#ls;Function (n.inc args') env bodyS') + (case (recur inner-arity resolver' +0 bodyA) + (#ls;Function arity' env' bodyS') + (let [arity (n.inc arity')] + (#ls;Function arity env (prepare-body inner-arity arity bodyS'))) bodyS - (#ls;Function +1 env bodyS))) - + (#ls;Function +1 env (prepare-body inner-arity +1 bodyS)))) + (#la;Apply _) (let [[funcA argsA] (&&function;unfold-apply exprA) - funcS (recur +0 resolver funcA) - argsS (L/map (recur +0 resolver) argsA)] + funcS (recur +0 resolver num-locals funcA) + argsS (L/map (recur +0 resolver num-locals) argsA)] (case funcS - ## (^multi (#ls;Variable idx) - ## (and (|> scope-args n.dec nat-to-int (i.* -1) (i.= idx)) - ## tail?)) - ## (#ls;Recur +1 argsS) - - ## (^multi (#ls;Function _scope-args _scope _bodyS) - ## (and (n.= _scope-args (list;size argsS)) - ## (not (has-self-reference? _bodyS)))) - ## (#ls;Loop local-offset argsS (shift-loop-variables local-offset _bodyS)) + (^multi (#ls;Function _arity _env _bodyS) + (and (n.= _arity (list;size argsS)) + (not (&&loop;contains-self-reference? _bodyS)))) + (let [register-offset (if (&&function;top? outer-arity) + num-locals + (|> outer-arity n.inc (n.+ num-locals)))] + (#ls;Loop register-offset argsS + (&&loop;adjust _env register-offset _bodyS))) + + (#ls;Call funcS' argsS') + (#ls;Call funcS' (L/append argsS' argsS)) _ (#ls;Call funcS argsS))) (#la;Procedure name args) - (#ls;Procedure name (L/map (recur +0 resolver) args)) + (#ls;Procedure name (L/map (recur +0 resolver num-locals) args)) _ (undefined) diff --git a/new-luxc/source/luxc/synthesizer/function.lux b/new-luxc/source/luxc/synthesizer/function.lux index be6a74da0..42aa7a6cd 100644 --- a/new-luxc/source/luxc/synthesizer/function.lux +++ b/new-luxc/source/luxc/synthesizer/function.lux @@ -22,18 +22,23 @@ (-> ls;Variable Bool) ( 0 var))] - [function-var? i.=] - [local-var? i.>] - [captured-var? i.<] + [self? i.=] + [local? i.>] + [captured? i.<] ) -(def: #export (nested-function? scope-args) - (-> Nat Bool) - (n.> +1 scope-args)) +(do-template [ ] + [(def: #export ( arity) + (-> ls;Arity Bool) + ( arity))] -(def: #export (adjust-var scope-args var) - (-> Nat ls;Variable ls;Variable) - (|> scope-args n.dec nat-to-int (i.+ var))) + [nested? n.> +1] + [top? n.= +0] + ) + +(def: #export (adjust-var outer var) + (-> ls;Arity ls;Variable ls;Variable) + (|> outer n.dec nat-to-int (i.+ var))) (def: #export (to-captured idx) (-> Nat Int) diff --git a/new-luxc/source/luxc/synthesizer/loop.lux b/new-luxc/source/luxc/synthesizer/loop.lux new file mode 100644 index 000000000..06b1d1bb0 --- /dev/null +++ b/new-luxc/source/luxc/synthesizer/loop.lux @@ -0,0 +1,166 @@ +(;module: + lux + (lux (data (coll [list "L/" Functor]) + text/format)) + (luxc (lang ["ls" synthesis]) + (synthesizer ["&&;" function]))) + +(def: #export (contains-self-reference? exprS) + (-> ls;Synthesis Bool) + (case exprS + (#ls;Variant tag last? memberS) + (contains-self-reference? memberS) + + (#ls;Tuple membersS) + (list;any? contains-self-reference? membersS) + + (#ls;Case inputS pathS) + (or (contains-self-reference? inputS) + (loop [pathS pathS] + (case pathS + (^or (#ls;AltP leftS rightS) + (#ls;SeqP leftS rightS)) + (or (recur leftS) + (recur rightS)) + + (#ls;ExecP bodyS) + (contains-self-reference? bodyS) + + _ + false))) + + (#ls;Function arity environment bodyS) + (list;any? &&function;self? environment) + + (#ls;Call funcS argsS) + (or (contains-self-reference? funcS) + (list;any? contains-self-reference? argsS)) + + (^or (#ls;Recur argsS) + (#ls;Procedure name argsS)) + (list;any? contains-self-reference? argsS) + + (#ls;Variable idx) + (&&function;self? idx) + + (#ls;Let register inputS bodyS) + (or (contains-self-reference? inputS) + (contains-self-reference? bodyS)) + + (#ls;If inputS thenS elseS) + (or (contains-self-reference? inputS) + (contains-self-reference? thenS) + (contains-self-reference? elseS)) + + (#ls;Loop offset argsS bodyS) + (or (list;any? contains-self-reference? argsS) + (contains-self-reference? bodyS)) + + _ + false + )) + +(def: #export (reify-recursion arity exprS) + (-> Nat ls;Synthesis ls;Synthesis) + (loop [exprS exprS] + (case exprS + (#ls;Case inputS pathS) + (#ls;Case inputS + (let [reify-recursion' recur] + (loop [pathS pathS] + (case pathS + (#ls;AltP leftS rightS) + (#ls;AltP (recur leftS) (recur rightS)) + + (#ls;SeqP leftS rightS) + (#ls;SeqP leftS (recur rightS)) + + (#ls;ExecP bodyS) + (#ls;ExecP (reify-recursion' bodyS)) + + _ + pathS)))) + + (^multi (#ls;Call (#ls;Variable 0) argsS) + (n.= arity (list;size argsS))) + (#ls;Recur argsS) + + (#ls;Call (#ls;Variable var) argsS) + exprS + + (#ls;Let register inputS bodyS) + (#ls;Let register inputS (recur bodyS)) + + (#ls;If inputS thenS elseS) + (#ls;If inputS + (recur thenS) + (recur elseS)) + + _ + exprS + ))) + +(def: #export (adjust env outer-offset exprS) + (-> (List ls;Variable) ls;Register ls;Synthesis ls;Synthesis) + (let [resolve-captured (: (-> ls;Variable ls;Variable) + (function [var] + (let [idx (|> var (i.* -1) int-to-nat n.dec)] + (|> env (list;nth idx) assume))))] + (loop [exprS exprS] + (case exprS + (#ls;Variant tag last? valueS) + (#ls;Variant tag last? (recur valueS)) + + (#ls;Tuple members) + (#ls;Tuple (L/map recur members)) + + (#ls;Case inputS pathS) + (#ls;Case (recur inputS) + (let [adjust' recur] + (loop [pathS pathS] + (case pathS + (^template [] + ( leftS rightS) + ( (recur leftS) (recur rightS))) + ([#ls;AltP] + [#ls;SeqP]) + + (#ls;ExecP bodyS) + (#ls;ExecP (adjust' bodyS)) + + _ + pathS)))) + + (#ls;Function arity scope bodyS) + (#ls;Function arity + (L/map resolve-captured scope) + (recur bodyS)) + + (#ls;Call funcS argsS) + (#ls;Call (recur funcS) (L/map recur argsS)) + + (#ls;Recur argsS) + (#ls;Recur (L/map recur argsS)) + + (#ls;Procedure name argsS) + (#ls;Procedure name (L/map recur argsS)) + + (#ls;Variable var) + (if (&&function;captured? var) + (#ls;Variable (resolve-captured var)) + (#ls;Variable (|> outer-offset nat-to-int (i.+ var)))) + + (#ls;Let register inputS bodyS) + (#ls;Let (n.+ outer-offset register) (recur inputS) (recur bodyS)) + + (#ls;If inputS thenS elseS) + (#ls;If (recur inputS) (recur thenS) (recur elseS)) + + (#ls;Loop inner-offset argsS bodyS) + (#ls;Loop (n.+ outer-offset inner-offset) + (L/map recur argsS) + (recur bodyS)) + + _ + exprS + )))) diff --git a/new-luxc/test/test/luxc/synthesizer/function.lux b/new-luxc/test/test/luxc/synthesizer/function.lux index 7c4776727..6ad7ed634 100644 --- a/new-luxc/test/test/luxc/synthesizer/function.lux +++ b/new-luxc/test/test/luxc/synthesizer/function.lux @@ -13,14 +13,13 @@ test) (luxc (lang ["la" analysis] ["ls" synthesis]) - (analyser [";A" structure]) [synthesizer] (synthesizer ["&&;" function])) (.. common)) (def: (reference var) (-> ls;Variable Ref) - (if (&&function;captured-var? var) + (if (&&function;captured? var) (#;Captured (|> var (i.* -1) int-to-nat n.dec)) (#;Local (int-to-nat var)))) diff --git a/new-luxc/test/test/luxc/synthesizer/loop.lux b/new-luxc/test/test/luxc/synthesizer/loop.lux new file mode 100644 index 000000000..b89e09659 --- /dev/null +++ b/new-luxc/test/test/luxc/synthesizer/loop.lux @@ -0,0 +1,164 @@ +(;module: + lux + (lux [io] + (control monad) + (data [bool "B/" Eq] + [number] + (coll [list "L/" Functor Fold] + ["s" set]) + text/format) + ["r" math/random "r/" Monad] + test) + (luxc (lang ["la" analysis] + ["ls" synthesis]) + [synthesizer] + (synthesizer ["&&;" loop])) + (.. common)) + +(def: (does-recursion? arity exprS) + (-> ls;Arity ls;Synthesis Bool) + (loop [exprS exprS] + (case exprS + (#ls;Case inputS pathS) + (loop [pathS pathS] + (case pathS + (#ls;AltP leftS rightS) + (or (recur leftS) + (recur rightS)) + + (#ls;SeqP leftS rightS) + (recur rightS) + + (#ls;ExecP bodyS) + (does-recursion? arity bodyS) + + _ + false)) + + (#ls;Recur argsS) + (n.= arity (list;size argsS)) + + (#ls;Let register inputS bodyS) + (recur bodyS) + + (#ls;If inputS thenS elseS) + (or (recur thenS) + (recur elseS)) + + _ + false + ))) + +(def: (gen-body arity output) + (-> Nat la;Analysis (r;Random la;Analysis)) + (r;either (r;either (r/wrap output) + (do r;Monad + [inputA (|> r;nat (:: @ map (|>. #la;Nat))) + num-cases (|> r;nat (:: @ map (|>. (n.% +10) (n.max +1)))) + tests (|> (r;set number;Hash num-cases r;nat) + (:: @ map (|>. s;to-list (L/map (|>. #la;NatP))))) + #let [bad-bodies (list;repeat num-cases #la;Unit)] + good-body (gen-body arity output) + where-to-set (|> r;nat (:: @ map (n.% num-cases))) + #let [bodies (list;concat (list (list;take where-to-set bad-bodies) + (list good-body) + (list;drop (n.inc where-to-set) bad-bodies)))]] + (wrap (#ls;Case inputA + (list;zip2 tests bodies))))) + (r;either (do r;Monad + [valueS r;bool + output' (gen-body (n.inc arity) output)] + (wrap (#la;Case (#la;Bool valueS) (list [(#la;BindP arity) output'])))) + (do r;Monad + [valueS r;bool + then|else r;bool + output' (gen-body arity output) + #let [thenA (if then|else output' #ls;Unit) + elseA (if (not then|else) output' #ls;Unit)]] + (wrap (#la;Case (#la;Bool valueS) + (list [(#la;BoolP then|else) thenA] + [(#la;BoolP (not then|else)) elseA]))))) + )) + +(def: (make-apply func args) + (-> la;Analysis (List la;Analysis) la;Analysis) + (L/fold (function [arg' func'] + (#la;Apply arg' func')) + func + args)) + +(def: (make-function arity body) + (-> ls;Arity la;Analysis la;Analysis) + (case arity + +0 body + _ (#la;Function {#;name (list) + #;inner +0 + #;locals {#;counter +0 #;mappings (list)} + #;captured {#;counter +0 #;mappings (list)}} + (make-function (n.dec arity) body)))) + +(def: gen-recursion + (r;Random [Bool Nat la;Analysis]) + (do r;Monad + [arity (|> r;nat (:: @ map (|>. (n.% +10) (n.max +1)))) + recur? r;bool + outputS (if recur? + (wrap (make-apply (#la;Relative (#;Local +0)) + (list;repeat arity #la;Unit))) + (do @ + [plus-or-minus? r;bool + how-much (|> r;nat (:: @ map (|>. (n.% arity) (n.max +1)))) + #let [shift (if plus-or-minus? n.+ n.-)]] + (wrap (make-apply (#la;Relative (#;Local +0)) + (list;repeat (shift how-much arity) #la;Unit))))) + bodyS (gen-body arity outputS)] + (wrap [recur? arity (make-function arity bodyS)]))) + +(def: gen-loop + (r;Random [Bool Nat la;Analysis]) + (do r;Monad + [arity (|> r;nat (:: @ map (|>. (n.% +10) (n.max +1)))) + recur? r;bool + self-ref? r;bool + #let [selfA (#la;Relative (#;Local +0)) + argA (if self-ref? selfA #la;Unit)] + outputS (if recur? + (wrap (make-apply selfA (list;repeat arity argA))) + (do @ + [plus-or-minus? r;bool + how-much (|> r;nat (:: @ map (|>. (n.% arity) (n.max +1)))) + #let [shift (if plus-or-minus? n.+ n.-)]] + (wrap (make-apply selfA (list;repeat (shift how-much arity) argA))))) + bodyS (gen-body arity outputS)] + (wrap [(and recur? (not self-ref?)) + arity + (make-function arity bodyS)]))) + +(test: "Recursion." + [[prediction arity analysis] gen-recursion] + ($_ seq + (assert "Can accurately identify (and then reify) tail recursion." + (case (synthesizer;synthesize analysis) + (#ls;Function _arity _env _body) + (|> _body + (does-recursion? arity) + (B/= prediction) + (and (n.= arity _arity))) + + _ + false)))) + +(test: "Loop." + [[prediction arity analysis] gen-recursion] + ($_ seq + (assert "Can reify loops." + (case (synthesizer;synthesize (make-apply analysis (list;repeat arity #la;Unit))) + (#ls;Loop _register _inits _body) + (and (n.= arity (list;size _inits)) + (not (&&loop;contains-self-reference? _body))) + + (#ls;Call (#ls;Function _arity _env _bodyS) argsS) + (&&loop;contains-self-reference? _bodyS) + + _ + false)))) diff --git a/new-luxc/test/tests.lux b/new-luxc/test/tests.lux index 114768c2d..30a8ec522 100644 --- a/new-luxc/test/tests.lux +++ b/new-luxc/test/tests.lux @@ -15,7 +15,8 @@ (synthesizer ["_;S" primitive] ["_;S" structure] ["_;S" function] - ["_;S" procedure])))) + ["_;S" procedure] + ["_;S" loop])))) ## [Program] (program: args -- cgit v1.2.3