diff options
Diffstat (limited to 'stdlib')
| -rw-r--r-- | stdlib/source/lux/math/simple.lux | 330 | ||||
| -rw-r--r-- | stdlib/source/lux/type/check.lux | 96 |
2 files changed, 378 insertions, 48 deletions
diff --git a/stdlib/source/lux/math/simple.lux b/stdlib/source/lux/math/simple.lux new file mode 100644 index 000000000..f6adbc162 --- /dev/null +++ b/stdlib/source/lux/math/simple.lux @@ -0,0 +1,330 @@ +## Copyright (c) Eduardo Julian. All rights reserved. +## This Source Code Form is subject to the terms of the Mozilla Public License, v. 2.0. +## If a copy of the MPL was not distributed with this file, +## You can obtain one at http://mozilla.org/MPL/2.0/. + +(;module: + lux + (lux (control monad) + (data text/format) + [compiler] + (macro [ast] + ["s" syntax #+ syntax: Syntax]) + [type] + (type [check]))) + +(do-template [<name> <rec> <nat-op> <int-op> <real-op> <frac-op>] + [(syntax: #export (<name> {args ($_ s;alt + (s;seq s;symbol s;symbol) + (s;seq s;any s;any) + s;symbol + s;any + s;end)}) + (case args + (+0 [x y]) + (do @ + [=x (compiler;find-type x) + =y (compiler;find-type y) + op (cond (and (check;checks? Nat =x) + (check;checks? Nat =y)) + (wrap (` <nat-op>)) + + (and (check;checks? Int =x) + (check;checks? Int =y)) + (wrap (` <int-op>)) + + (and (check;checks? Real =x) + (check;checks? Real =y)) + (wrap (` <real-op>)) + + (and (check;checks? Frac =x) + (check;checks? Frac =y)) + (wrap (` <frac-op>)) + + (compiler;fail (format "No operation for types: " (%type =x) " and " (%type =y))))] + (wrap (list (` ((~ op) (~ (ast;symbol x)) (~ (ast;symbol y))))))) + + (+1 [x y]) + (do @ + [g!x (compiler;gensym "g!x") + g!y (compiler;gensym "g!y")] + (wrap (list (` (let [(~ g!x) (~ x) + (~ g!y) (~ y)] + (<rec> (~ g!x) (~ g!y))))))) + + (+2 x) + (do @ + [=x (compiler;find-type x) + op (cond (check;checks? Nat =x) + (wrap (` <nat-op>)) + + (check;checks? Int =x) + (wrap (` <int-op>)) + + (check;checks? Real =x) + (wrap (` <real-op>)) + + (check;checks? Frac =x) + (wrap (` <frac-op>)) + + (compiler;fail (format "No operation for type: " (%type =x))))] + (wrap (list (` ((~ op) (~ (ast;symbol x))))))) + + (+3 x) + (do @ + [g!x (compiler;gensym "g!x")] + (wrap (list (` (let [(~ g!x) (~ x)] + (<rec> (~ g!x))))))) + + (+4 []) + (do @ + [=e compiler;expected-type + op (cond (check;checks? (-> Nat Nat Nat) =e) + (wrap (` <nat-op>)) + + (check;checks? (-> Int Int Int) =e) + (wrap (` <int-op>)) + + (check;checks? (-> Real Real Real) =e) + (wrap (` <real-op>)) + + (check;checks? (-> Frac Frac Frac) =e) + (wrap (` <frac-op>)) + + (compiler;fail (format "No operation for type: " (%type =e))))] + (wrap (list op))) + ))] + + [+ ;;+ n.+ i.+ r.+ f.+] + [- ;;- n.- i.- r.- f.-] + [* ;;* n.* i.* r.* f.*] + [/ ;;/ n./ i./ r./ f./] + [% ;;% n.% i.% r.% f.%] + ) + +(do-template [<name> <rec> <nat-op> <int-op> <real-op>] + [(syntax: #export (<name> {args ($_ s;alt + (s;seq s;symbol s;symbol) + (s;seq s;any s;any) + s;symbol + s;any + s;end)}) + (case args + (+0 [x y]) + (do @ + [=x (compiler;find-type x) + =y (compiler;find-type y) + op (cond (and (check;checks? Nat =x) + (check;checks? Nat =y)) + (wrap (` <nat-op>)) + + (and (check;checks? Int =x) + (check;checks? Int =y)) + (wrap (` <int-op>)) + + (and (check;checks? Real =x) + (check;checks? Real =y)) + (wrap (` <real-op>)) + + (compiler;fail (format "No operation for types: " (%type =x) " and " (%type =y))))] + (wrap (list (` ((~ op) (~ (ast;symbol x)) (~ (ast;symbol y))))))) + + (+1 [x y]) + (do @ + [g!x (compiler;gensym "g!x") + g!y (compiler;gensym "g!y")] + (wrap (list (` (let [(~ g!x) (~ x) + (~ g!y) (~ y)] + (<rec> (~ g!x) (~ g!y))))))) + + (+2 x) + (do @ + [=x (compiler;find-type x) + op (cond (check;checks? Nat =x) + (wrap (` <nat-op>)) + + (check;checks? Int =x) + (wrap (` <int-op>)) + + (check;checks? Real =x) + (wrap (` <real-op>)) + + (compiler;fail (format "No operation for type: " (%type =x))))] + (wrap (list (` ((~ op) (~ (ast;symbol x))))))) + + (+3 x) + (do @ + [g!x (compiler;gensym "g!x")] + (wrap (list (` (let [(~ g!x) (~ x)] + (<rec> (~ g!x))))))) + + (+4 []) + (do @ + [=e compiler;expected-type + op (cond (check;checks? (-> Nat Nat Nat) =e) + (wrap (` <nat-op>)) + + (check;checks? (-> Int Int Int) =e) + (wrap (` <int-op>)) + + (check;checks? (-> Real Real Real) =e) + (wrap (` <real-op>)) + + (compiler;fail (format "No operation for type: " (%type =e))))] + (wrap (list op))) + ))] + + [= ;;= n.= i.= r.=] + [< ;;< n.< i.< r.<] + [<= ;;<= n.<= i.<= r.<=] + [> ;;> n.> i.> r.>] + [>= ;;>= n.>= i.>= r.>=] + ) + +(do-template [<name> <rec> <nat-op> <int-op>] + [(syntax: #export (<name> {args ($_ s;alt + (s;seq s;symbol s;symbol) + (s;seq s;any s;any) + s;symbol + s;any + s;end)}) + (case args + (+0 [x y]) + (do @ + [=x (compiler;find-type x) + =y (compiler;find-type y) + op (cond (and (check;checks? Nat =x) + (check;checks? Nat =y)) + (wrap (` <nat-op>)) + + (and (check;checks? Int =x) + (check;checks? Int =y)) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for types: " (%type =x) " and " (%type =y))))] + (wrap (list (` ((~ op) (~ (ast;symbol x)) (~ (ast;symbol y))))))) + + (+1 [x y]) + (do @ + [g!x (compiler;gensym "g!x") + g!y (compiler;gensym "g!y")] + (wrap (list (` (let [(~ g!x) (~ x) + (~ g!y) (~ y)] + (<rec> (~ g!x) (~ g!y))))))) + + (+2 x) + (do @ + [=x (compiler;find-type x) + op (cond (check;checks? Nat =x) + (wrap (` <nat-op>)) + + (check;checks? Int =x) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for type: " (%type =x))))] + (wrap (list (` ((~ op) (~ (ast;symbol x))))))) + + (+3 x) + (do @ + [g!x (compiler;gensym "g!x")] + (wrap (list (` (let [(~ g!x) (~ x)] + (<rec> (~ g!x))))))) + + (+4 []) + (do @ + [=e compiler;expected-type + op (cond (check;checks? (-> Nat Nat Nat) =e) + (wrap (` <nat-op>)) + + (check;checks? (-> Int Int Int) =e) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for type: " (%type =e))))] + (wrap (list op))) + ))] + + [min ;;min n.min i.min] + [max ;;max n.max i.max] + ) + +(do-template [<name> <rec> <nat-op> <int-op>] + [(syntax: #export (<name> {args ($_ s;alt + s;symbol + s;any + s;end)}) + (case args + (+0 x) + (do @ + [=x (compiler;find-type x) + op (cond (check;checks? Nat =x) + (wrap (` <nat-op>)) + + (check;checks? Int =x) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for type: " (%type =x))))] + (wrap (list (` ((~ op) (~ (ast;symbol x))))))) + + (+1 x) + (do @ + [g!x (compiler;gensym "g!x")] + (wrap (list (` (let [(~ g!x) (~ x)] + (<rec> (~ g!x))))))) + + (+2 []) + (do @ + [=e compiler;expected-type + op (cond (check;checks? (-> Nat Nat) =e) + (wrap (` <nat-op>)) + + (check;checks? (-> Int Int) =e) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for type: " (%type =e))))] + (wrap (list op))) + ))] + + [inc ;;inc n.inc i.inc] + [dec ;;dec n.dec i.dec] + ) + +(do-template [<name> <rec> <nat-op> <int-op>] + [(syntax: #export (<name> {args ($_ s;alt + s;symbol + s;any + s;end)}) + (case args + (+0 x) + (do @ + [=x (compiler;find-type x) + op (cond (check;checks? Nat =x) + (wrap (` <nat-op>)) + + (check;checks? Int =x) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for type: " (%type =x))))] + (wrap (list (` ((~ op) (~ (ast;symbol x))))))) + + (+1 x) + (do @ + [g!x (compiler;gensym "g!x")] + (wrap (list (` (let [(~ g!x) (~ x)] + (<rec> (~ g!x))))))) + + (+2 []) + (do @ + [=e compiler;expected-type + op (cond (check;checks? (-> Nat Bool) =e) + (wrap (` <nat-op>)) + + (check;checks? (-> Int Bool) =e) + (wrap (` <int-op>)) + + (compiler;fail (format "No operation for type: " (%type =e))))] + (wrap (list op))) + ))] + + [even? ;;even? n.even? i.even?] + [odd? ;;odd? n.odd? i.odd?] + ) diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux index b4d90e004..3291f3f56 100644 --- a/stdlib/source/lux/type/check.lux +++ b/stdlib/source/lux/type/check.lux @@ -12,6 +12,7 @@ text/format [number] maybe + [product] (struct [list] [dict]) error) @@ -214,22 +215,22 @@ (wrap (#;HostT name =params))) (^template [<tag>] - (<tag> left right) - (do Monad<Check> - [=left (clean t-id left) - =right (clean t-id right)] - (wrap (<tag> =left =right)))) + (<tag> left right) + (do Monad<Check> + [=left (clean t-id left) + =right (clean t-id right)] + (wrap (<tag> =left =right)))) ([#;LambdaT] [#;AppT] [#;ProdT] [#;SumT]) (^template [<tag>] - (<tag> env body) - (do Monad<Check> - [=env (mapM @ (clean t-id) env) - =body (clean t-id body)] ## TODO: DON'T CLEAN THE BODY - (wrap (<tag> =env =body)))) + (<tag> env body) + (do Monad<Check> + [=env (mapM @ (clean t-id) env) + =body (clean t-id body)] ## TODO: DON'T CLEAN THE BODY + (wrap (<tag> =env =body)))) ([#;UnivQ] [#;ExQ]) @@ -334,7 +335,7 @@ (def: success (Check []) (Check/wrap [])) -(def: (|| left right) +(def: (either left right) (All [a] (-> (Check a) (Check a) (Check a))) (lambda [context] (case (left context) @@ -346,12 +347,11 @@ (def: (fp-get [e a] fixpoints) (-> [Type Type] Fixpoints (Maybe Bool)) - (list;find (lambda [[[fe fa] status]] - (if (and (Type/= e fe) - (Type/= a fa)) - (#;Some status) - #;None)) - fixpoints)) + (:: Monad<Maybe> map product;right + (list;find (lambda [[[fe fa] status]] + (and (Type/= e fe) + (Type/= a fa))) + fixpoints))) (def: (fp-put ea status fixpoints) (-> [Type Type] Bool Fixpoints Fixpoints) @@ -382,16 +382,16 @@ (check etype atype)))) [(#;VarT id) _] - (|| (set-var id actual) - (do Monad<Check> - [bound (deref id)] - (check bound actual))) + (either (set-var id actual) + (do Monad<Check> + [bound (deref id)] + (check bound actual))) [_ (#;VarT id)] - (|| (set-var id expected) - (do Monad<Check> - [bound (deref id)] - (check expected bound))) + (either (set-var id expected) + (do Monad<Check> + [bound (deref id)] + (check expected bound))) [(#;AppT (#;ExT eid) eA) (#;AppT (#;ExT aid) aA)] (if (n.= eid aid) @@ -399,24 +399,24 @@ (fail-check expected actual)) [(#;AppT (#;VarT id) A1) (#;AppT F2 A2)] - (|| (do Monad<Check> - [F1 (deref id)] - (check (#;AppT F1 A1) actual)) - (do Monad<Check> - [_ (check (#;VarT id) F2) - e' (apply-type! F2 A1) - a' (apply-type! F2 A2)] - (check e' a'))) + (either (do Monad<Check> + [F1 (deref id)] + (check (#;AppT F1 A1) actual)) + (do Monad<Check> + [_ (check (#;VarT id) F2) + e' (apply-type! F2 A1) + a' (apply-type! F2 A2)] + (check e' a'))) [(#;AppT F1 A1) (#;AppT (#;VarT id) A2)] - (|| (do Monad<Check> - [F2 (deref id)] - (check expected (#;AppT F2 A2))) - (do Monad<Check> - [_ (check F1 (#;VarT id)) - e' (apply-type! F1 A1) - a' (apply-type! F1 A2)] - (check e' a'))) + (either (do Monad<Check> + [F2 (deref id)] + (check expected (#;AppT F2 A2))) + (do Monad<Check> + [_ (check F1 (#;VarT id)) + e' (apply-type! F1 A1) + a' (apply-type! F1 A2)] + (check e' a'))) [(#;AppT F A) _] (do Monad<Check> @@ -479,13 +479,13 @@ (fail-check expected actual)) (^template [<unit> <append>] - [<unit> <unit>] - success - - [(<append> eL eR) (<append> aL aR)] - (do Monad<Check> - [_ (check eL aL)] - (check eR aR))) + [<unit> <unit>] + success + + [(<append> eL eR) (<append> aL aR)] + (do Monad<Check> + [_ (check eL aL)] + (check eR aR))) ([#;VoidT #;SumT] [#;UnitT #;ProdT]) |