diff options
Diffstat (limited to 'source/lux')
| -rw-r--r-- | source/lux/codata/stream.lux | 2 | ||||
| -rw-r--r-- | source/lux/control/comonad.lux | 2 | ||||
| -rw-r--r-- | source/lux/data/bool.lux | 2 | ||||
| -rw-r--r-- | source/lux/data/list.lux | 160 | ||||
| -rw-r--r-- | source/lux/data/text.lux | 17 | ||||
| -rw-r--r-- | source/lux/host/io.lux | 22 | ||||
| -rw-r--r-- | source/lux/host/jvm.lux | 151 | ||||
| -rw-r--r-- | source/lux/meta/ast.lux | 60 | ||||
| -rw-r--r-- | source/lux/meta/lux.lux | 4 | ||||
| -rw-r--r-- | source/lux/meta/syntax.lux | 2 | ||||
| -rw-r--r-- | source/lux/meta/type.lux | 82 |
11 files changed, 168 insertions, 336 deletions
diff --git a/source/lux/codata/stream.lux b/source/lux/codata/stream.lux index e2464248c..96de64fd4 100644 --- a/source/lux/codata/stream.lux +++ b/source/lux/codata/stream.lux @@ -105,7 +105,7 @@ (def #export (partition p xs) (All [a] (-> (-> a Bool) (Stream a) (, (Stream a) (Stream a)))) - [(filter p xs) (filter (complement p) xs)]) + [(filter p xs) (filter (comp p) xs)]) ## [Structures] (defstruct #export Stream/Functor (Functor Stream) diff --git a/source/lux/control/comonad.lux b/source/lux/control/comonad.lux index 32e7c64c1..7ea3b58a9 100644 --- a/source/lux/control/comonad.lux +++ b/source/lux/control/comonad.lux @@ -5,7 +5,7 @@ (;import lux (../functor #as F) - lux/data/list) + (lux/data/list #refer #all #open ("" List/Fold))) ## [Signatures] (defsig #export (CoMonad w) diff --git a/source/lux/data/bool.lux b/source/lux/data/bool.lux index defaee22e..a3e28733b 100644 --- a/source/lux/data/bool.lux +++ b/source/lux/data/bool.lux @@ -31,6 +31,6 @@ ) ## [Functions] -(def #export complement +(def #export comp (All [a] (-> (-> a Bool) (-> a Bool))) (. not)) diff --git a/source/lux/data/list.lux b/source/lux/data/list.lux index 8a7f97698..54f8fed4c 100644 --- a/source/lux/data/list.lux +++ b/source/lux/data/list.lux @@ -10,8 +10,11 @@ (eq #as E) (ord #as O) (fold #as f)) - (data (number (int #open ("i" Int/Number Int/Ord))) - bool))) + (data (number (int #open ("i:" Int/Number Int/Ord Int/Show))) + bool + (text #open ("text:" Text/Monoid)) + tuple) + codata/function)) ## [Types] ## (deftype (List a) @@ -19,26 +22,6 @@ ## (#Cons (, a (List a))))) ## [Functions] -(def #export (foldL f init xs) - (All [a b] - (-> (-> a b a) a (List b) a)) - (case xs - #;Nil - init - - (#;Cons [x xs']) - (foldL f (f init x) xs'))) - -(def #export (foldR f init xs) - (All [a b] - (-> (-> b a a) a (List b) a)) - (case xs - #;Nil - init - - (#;Cons [x xs']) - (f x (foldR f init xs')))) - (defstruct #export List/Fold (f;Fold List) (def (foldL f init xs) (case xs @@ -56,6 +39,8 @@ (#;Cons [x xs']) (f x (foldR f init xs'))))) +(open List/Fold) + (def #export (fold mon xs) (All [a] (-> (m;Monoid a) (List a) a)) @@ -83,7 +68,7 @@ (def #export (partition p xs) (All [a] (-> (-> a Bool) (List a) (, (List a) (List a)))) - [(filter p xs) (filter (complement p) xs)]) + [(filter p xs) (filter (comp p) xs)]) (def #export (as-pairs xs) (All [a] (-> (List a) (List (, a a)))) @@ -98,7 +83,7 @@ [(def #export (<name> n xs) (All [a] (-> Int (List a) (List a))) - (if (i> n 0) + (if (i:> n 0) (case xs #;Nil #;Nil @@ -107,8 +92,8 @@ <then>) <else>))] - [take (#;Cons [x (take (i+ -1 n) xs')]) #;Nil] - [drop (drop (i+ -1 n) xs') xs] + [take (#;Cons [x (take (i:+ -1 n) xs')]) #;Nil] + [drop (drop (i:+ -1 n) xs') xs] ) (do-template [<name> <then> <else>] @@ -131,13 +116,13 @@ (def #export (split n xs) (All [a] (-> Int (List a) (, (List a) (List a)))) - (if (i> n 0) + (if (i:> n 0) (case xs #;Nil [#;Nil #;Nil] (#;Cons [x xs']) - (let [[tail rest] (split (i+ -1 n) xs')] + (let [[tail rest] (split (i:+ -1 n) xs')] [(#;Cons [x tail]) rest])) [#;Nil xs])) @@ -162,8 +147,8 @@ (def #export (repeat n x) (All [a] (-> Int a (List a))) - (if (i> n 0) - (#;Cons [x (repeat (i+ -1 n) x)]) + (if (i:> n 0) + (#;Cons [x (repeat (i:+ -1 n) x)]) #;Nil)) (def #export (iterate f x) @@ -206,7 +191,7 @@ (def #export (size list) (-> List Int) - (foldL (lambda [acc _] (i+ 1 acc)) 0 list)) + (foldL (lambda [acc _] (i:+ 1 acc)) 0 list)) (do-template [<name> <init> <op>] [(def #export (<name> p xs) @@ -225,9 +210,9 @@ #;None (#;Cons [x xs']) - (if (i= 0 i) + (if (i:= 0 i) (#;Some x) - (@ (i+ -1 i) xs')))) + (@ (i:+ -1 i) xs')))) ## [Syntax] (defmacro #export (@list xs state) @@ -248,68 +233,6 @@ _ (#;Left "Wrong syntax for @list&"))) -## (defmacro #export (zip tokens state) -## (if (i> (size tokens) 0) -## (using List/Functor -## (let [indices (range 0 (i+ 1 (size tokens))) -## vars+lists (map (lambda [idx] -## (let [base (text:++ "_" idx)] -## [[["" -1 -1] (#SymbolS "" base)] -## [["" -1 -1] (#SymbolS "" (text:++ base "s"))]])) -## indices) -## pattern (` [(~@ (map (lambda [[v vs]] (` (#;Cons (~ v) (~ vs)))) -## vars+lists))]) -## g!step [["" -1 -1] (#SymbolS "" "\tstep\t")] -## g!arg [["" -1 -1] (#SymbolS "" "\targ\t")] -## g!blank [["" -1 -1] (#SymbolS "" "\t_\t")] -## code (` ((lambda (~ g!step) [(~ g!arg)] -## (case (~ g!arg) -## (~ pattern) -## (#;Cons [(~@ vars)] ((~ g!step) [(~ (map second vars))])) - -## (~ g!blank) -## #;Nil)) -## [(~@ tokens)]))] -## (#;Right state (@list code)))) -## (#;Left "Can't zip no lists."))) - -## (defmacro #export (zip-with tokens state) -## (case tokens -## (@list& _f tokens) -## (case _f -## [_ (#;SymbolS _)] -## (if (i> (size tokens) 0) -## (using List/Functor -## (let [indices (range 0 (i+ 1 (size tokens))) -## vars+lists (map (lambda [idx] -## (let [base (text:++ "_" idx)] -## [[["" -1 -1] (#SymbolS "" base)] -## [["" -1 -1] (#SymbolS "" (text:++ base "s"))]])) -## indices) -## pattern (` [(~@ (map (lambda [[v vs]] (` (#;Cons (~ v) (~ vs)))) -## vars+lists))]) -## g!step [["" -1 -1] (#SymbolS "" "\tstep\t")] -## g!arg [["" -1 -1] (#SymbolS "" "\targ\t")] -## g!blank [["" -1 -1] (#SymbolS "" "\t_\t")] -## code (` ((lambda (~ g!step) [(~ g!arg)] -## (case (~ g!arg) -## (~ pattern) -## (#;Cons ((~ _f) (~@ vars)) ((~ g!step) [(~ (map second vars))])) - -## (~ g!blank) -## #;Nil)) -## [(~@ tokens)]))] -## (#;Right state (@list code)))) -## (#;Left "Can't zip-with no lists.")) - -## _ -## (let [g!temp [["" -1 -1] (#SymbolS "" "\ttemp\t")]] -## (#;Right state (@list (` (let [(~ g!temp) (~ _f)] -## (;;zip-with (~@ (@list& g!temp tokens))))))))) - -## _ -## (#;Left "Wrong syntax for zip-with"))) - ## [Structures] (defstruct #export (List/Eq eq) (All [a] (-> (E;Eq a) (E;Eq (List a)))) @@ -363,3 +286,50 @@ post (filter (< x) xs') ++ (:: List/Monoid m;++)] ($ ++ (sort ord pre) (@list x) (sort ord post)))))) + +## [Syntax] +(def (symbol$ name) + (-> Text AST) + [["" -1 -1] (#;SymbolS "" name)]) + +(def (range from to) + (-> Int Int (List Int)) + (if (i:<= from to) + (@list& from (range (i:+ 1 from) to)) + (@list))) + +(defmacro #export (zip tokens state) + (case tokens + (\ (@list [_ (#;IntS num-lists)])) + (if (i:> num-lists 0) + (using List/Functor + (let [indices (range 0 (i:- num-lists 1)) + type-vars (: (List AST) (map (. symbol$ i:show) indices)) + zip-type (` (All [(~@ type-vars)] + (-> (~@ (map (: (-> AST AST) (lambda [var] (` (List (~ var))))) + type-vars)) + (List (, (~@ type-vars)))))) + vars+lists (map (lambda [idx] + (let [base (text:++ "_" (i:show idx))] + [(symbol$ base) + (symbol$ (text:++ base "s"))])) + indices) + pattern (` [(~@ (map (lambda [[v vs]] (` (#;Cons (~ v) (~ vs)))) + vars+lists))]) + g!step (symbol$ "\tstep\t") + g!blank (symbol$ "\t_\t") + list-vars (map second vars+lists) + code (` (: (~ zip-type) + (lambda (~ g!step) [(~@ list-vars)] + (case [(~@ list-vars)] + (~ pattern) + (#;Cons [(~@ (map first vars+lists))] + ((~ g!step) (~@ list-vars))) + + (~ g!blank) + #;Nil))))] + (#;Right [state (@list code)]))) + (#;Left "Can't zip no lists.")) + + _ + (#;Left "Wrong syntax for zip"))) diff --git a/source/lux/data/text.lux b/source/lux/data/text.lux index 6c3a3dfee..bbcb42d71 100644 --- a/source/lux/data/text.lux +++ b/source/lux/data/text.lux @@ -10,8 +10,7 @@ (show #as S) (monad #as M #refer #all)) (data (number (int #open ("i" Int/Number Int/Ord))) - maybe - (list #refer (#only foldL @list @list&))))) + maybe))) ## [Functions] (def #export (size x) @@ -164,18 +163,20 @@ (-> Text (List AST)) (case (extract-var template) (#;Some [pre var post]) - (@list& (text$ pre) (symbol$ ["" var]) - (unravel-template post)) + (#;Cons (text$ pre) + (#;Cons (symbol$ ["" var]) + (unravel-template post))) #;None - (@list (text$ template)))) + (#;Cons (text$ template) #;Nil))) (defmacro #export (<> tokens state) (case tokens - (\ (@list [_ (#;TextS template)])) + (#;Cons [_ (#;TextS template)] #;Nil) (let [++ (symbol$ ["" ""])] - (#;Right state (@list (` (;let [(~ ++) (;:: Text/Monoid m;++)] - (;$ (~ ++) (~@ (unravel-template template)))))))) + (#;Right state (#;Cons (` (;let [(~ ++) (;:: Text/Monoid m;++)] + (;$ (~ ++) (~@ (unravel-template template))))) + #;Nil))) _ (#;Left "Wrong syntax for <>"))) diff --git a/source/lux/host/io.lux b/source/lux/host/io.lux index 7611e41b7..7c017a62e 100644 --- a/source/lux/host/io.lux +++ b/source/lux/host/io.lux @@ -11,25 +11,25 @@ (do-template [<name> <method> <type> <class>] [(def #export (<name> x) (-> <type> (IO (,))) - (@io (.! (<method> [<class>] [x]) - (..? out java.lang.System))))] + (@io (_jvm_invokevirtual "java.io.PrintStream" <method> [<class>] + (_jvm_getstatic "java.lang.System" "out") [x])))] - [write-char print Char char] - [write print Text java.lang.String] - [write-line println Text java.lang.String]) + [write-char "print" Char "char"] + [write "print" Text "java.lang.String"] + [write-line "println" Text "java.lang.String"]) (do-template [<name> <type> <op>] [(def #export <name> (IO (Maybe <type>)) - (let [in (..? in java.lang.System) - reader (new java.io.InputStreamReader [java.io.InputStream] [in]) - buff-reader (new java.io.BufferedReader [java.io.Reader] [reader])] + (let [in (_jvm_getstatic "java.lang.System" "in") + reader (_jvm_new "java.io.InputStreamReader" ["java.io.InputStream"] [in]) + buff-reader (_jvm_new "java.io.BufferedReader" ["java.io.Reader"] [reader])] (@io (let [output (: (Either Text <type>) (try$ <op>))] - (exec (.! (close [] []) buff-reader) + (exec (_jvm_invokeinterface "java.io.Closeable" "close" [] buff-reader []) (case output (#;Left _) #;None (#;Right input) (#;Some input)))))))] - [read-char Char (_jvm_i2c (.! (read [] []) buff-reader))] - [read-line Text (.! (readLine [] []) buff-reader)] + [read-char Char (_jvm_i2c (_jvm_invokevirtual "java.io.BufferedReader" "read" [] buff-reader []))] + [read-line Text (_jvm_invokevirtual "java.io.BufferedReader" "readLine" [] buff-reader [])] ) diff --git a/source/lux/host/jvm.lux b/source/lux/host/jvm.lux index eddedfdc5..6f121a633 100644 --- a/source/lux/host/jvm.lux +++ b/source/lux/host/jvm.lux @@ -9,29 +9,13 @@ (monad #as M #refer (#only do))) (data (list #as l #refer #all #open ("" List/Functor)) (text #as text) - (number (int #open ("i" Int/Eq)))) + number/int) (meta lux ast syntax))) ## [Utils] ## Parsers -(def finally^ - (Parser AST) - (form^ (do Parser/Monad - [_ (symbol?^ ["" "finally"]) - expr id^] - (wrap expr)))) - -(def catch^ - (Parser (, Text Ident AST)) - (form^ (do Parser/Monad - [_ (symbol?^ ["" "catch"]) - ex-class local-symbol^ - ex symbol^ - expr id^] - (wrap [ex-class ex expr])))) - (def method-decl^ (Parser (, (List Text) Text (List Text) Text)) (form^ (do Parser/Monad @@ -66,38 +50,7 @@ body id^] (wrap [modifiers name inputs output body])))) -(def method-call^ - (Parser (, Text (List Text) (List AST))) - (form^ (do Parser/Monad - [method local-symbol^ - arity-classes (tuple^ (*^ local-symbol^)) - arity-args (tuple^ (*^ id^)) - _ (: (Parser (,)) - (if (i= (size arity-classes) - (size arity-args)) - (wrap []) - (lambda [_] #;None)))] - (wrap [method arity-classes arity-args]) - ))) - ## [Syntax] -(defsyntax #export (throw ex) - (emit (@list (` (;_jvm_throw (~ ex)))))) - -(defsyntax #export (try body [catches (*^ catch^)] [finally (?^ finally^)]) - (emit (@list (` (;_jvm_try (~ body) - (~@ (:: List/Monoid (m;++ (map (: (-> (, Text Ident AST) AST) - (lambda [catch] - (let [[class ex body] catch] - (` (;_jvm_catch (~ (text$ class)) (~ (symbol$ ex)) (~ body)))))) - catches) - (case finally - #;None - (@list) - - (#;Some finally) - (: (List AST) (@list (` (;_jvm_finally (~ finally)))))))))))))) - (defsyntax #export (definterface [name local-symbol^] [supers (tuple^ (*^ local-symbol^))] [members (*^ method-decl^)]) (let [members' (map (: (-> (, (List Text) Text (List Text) Text) AST) (lambda [member] @@ -138,113 +91,19 @@ [(~@ fields')] [(~@ methods')])))))) -(defsyntax #export (new [class local-symbol^] [arg-classes (tuple^ (*^ local-symbol^))] [args (tuple^ (*^ id^))]) - (emit (@list (` (;_jvm_new (~ (text$ class)) - [(~@ (map text$ arg-classes))] - [(~@ args)]))))) - -(defsyntax #export (instance? [class local-symbol^] obj) - (emit (@list (` (;_jvm_instanceof (~ (text$ class)) (~ obj)))))) - -(defsyntax #export (locking lock body) - (do Lux/Monad - [g!lock (gensym "") - g!body (gensym "") - g!_ (gensym "")] - (emit (@list (` (let [(~ g!lock) (~ lock) - (~ g!_) (;_jvm_monitorenter (~ g!lock)) - (~ g!body) (~ body) - (~ g!_) (;_jvm_monitorexit (~ g!lock))] - (~ g!body))))) - )) - -(defsyntax #export (null? obj) - (emit (@list (` (;_jvm_null? (~ obj)))))) - (defsyntax #export (program [args symbol^] body) (emit (@list (` (;_jvm_program (~ (symbol$ args)) (~ body)))))) -(defsyntax #export (.? [field local-symbol^] obj) - (case obj - [_ (#;SymbolS obj-name)] - (do Lux/Monad - [obj-type (find-var-type obj-name)] - (case obj-type - (#;DataT class) - (emit (@list (` (;_jvm_getfield (~ (text$ class)) (~ (text$ field)))))) - - _ - (fail "Can only get field from object."))) - - _ - (do Lux/Monad - [g!obj (gensym "")] - (emit (@list (` (let [(~ g!obj) (~ obj)] - (;;.? (~ (text$ field)) (~ g!obj))))))))) - -(defsyntax #export (.= [field local-symbol^] value obj) - (case obj - [_ (#;SymbolS obj-name)] - (do Lux/Monad - [obj-type (find-var-type obj-name)] - (case obj-type - (#;DataT class) - (emit (@list (` (;_jvm_putfield (~ (text$ class)) (~ (text$ field)) (~ value))))) - - _ - (fail "Can only set field of object."))) - - _ - (do Lux/Monad - [g!obj (gensym "")] - (emit (@list (` (let [(~ g!obj) (~ obj)] - (;;.= (~ (text$ field)) (~ value) (~ g!obj))))))))) - -(defsyntax #export (.! [call method-call^] obj) - (let [[m-name ?m-classes m-args] call] - (case obj - [_ (#;SymbolS obj-name)] - (do Lux/Monad - [obj-type (find-var-type obj-name)] - (case obj-type - (#;DataT class) - (emit (@list (` (;_jvm_invokevirtual (~ (text$ class)) (~ (text$ m-name)) [(~@ (map text$ ?m-classes))] - (~ obj) [(~@ m-args)])))) - - _ - (fail "Can only call method on object."))) - - _ - (do Lux/Monad - [g!obj (gensym "")] - (emit (@list (` (let [(~ g!obj) (~ obj)] - (;;.! ((~ (symbol$ ["" m-name])) - [(~@ (map (lambda [c] (symbol$ ["" c])) ?m-classes))] - [(~@ m-args)]) - (~ g!obj)))))))))) - -(defsyntax #export (..? [field local-symbol^] [class local-symbol^]) - (emit (@list (` (;_jvm_getstatic (~ (text$ class)) (~ (text$ field))))))) - -(defsyntax #export (..= [field local-symbol^] value [class local-symbol^]) - (emit (@list (` (;_jvm_putstatic (~ (text$ class)) (~ (text$ field)) (~ value)))))) - -(defsyntax #export (..! [call method-call^] [class local-symbol^]) - (let [[m-name m-classes m-args] call] - (emit (@list (` (;_jvm_invokestatic (~ (text$ class)) (~ (text$ m-name)) - [(~@ (map text$ m-classes))] - [(~@ m-args)])))))) - (defsyntax #export (->maybe expr) (do Lux/Monad [g!val (gensym "")] (emit (@list (` (let [(~ g!val) (~ expr)] - (if (null? (~ g!val)) + (if (;_jvm_null? (~ g!val)) #;None (#;Some (~ g!val))))))))) (defsyntax #export (try$ expr) - (emit (@list (` (try (#;Right (~ expr)) - (~ (' (catch java.lang.Exception e - (#;Left (_jvm_invokevirtual "java.lang.Throwable" "getMessage" [] e [])))))))))) + (emit (@list (` (;_jvm_try (#;Right (~ expr)) + (~ (' (_jvm_catch "java.lang.Exception" e + (#;Left (_jvm_invokevirtual "java.lang.Throwable" "getMessage" [] e [])))))))))) diff --git a/source/lux/meta/ast.lux b/source/lux/meta/ast.lux index 8d649cf4a..398acf6cc 100644 --- a/source/lux/meta/ast.lux +++ b/source/lux/meta/ast.lux @@ -12,7 +12,7 @@ char (text #refer (#only Text/Show Text/Eq) #open ("text:" Text/Monoid)) ident - (list #refer #all #open ("" List/Functor)) + (list #refer #all #open ("" List/Functor List/Fold)) ))) ## [Types] @@ -79,35 +79,35 @@ ($ text:++ "{" (|> pairs (map (lambda [[left right]] ($ text:++ (show left) " " (show right)))) (interpose "") (foldL text:++ text:unit)) "}") ))) -## (defstruct #export AST/Eq (Eq AST) -## (def (= x y) -## (case [x y] -## (\template [<tag> <struct>] -## [[[_ (<tag> x')] [_ (<tag> y')]] -## (:: <struct> (E;= x' y'))]) -## [[#;BoolS Bool/Eq] -## [#;IntS Int/Eq] -## [#;RealS Real/Eq] -## [#;CharS Char/Eq] -## [#;TextS Text/Eq] -## [#;SymbolS Ident/Eq] -## [#;TagS Ident/Eq]] +(defstruct #export AST/Eq (Eq AST) + (def (= x y) + (case [x y] + (\template [<tag> <struct>] + [[[_ (<tag> x')] [_ (<tag> y')]] + (:: <struct> (E;= x' y'))]) + [[#;BoolS Bool/Eq] + [#;IntS Int/Eq] + [#;RealS Real/Eq] + [#;CharS Char/Eq] + [#;TextS Text/Eq] + [#;SymbolS Ident/Eq] + [#;TagS Ident/Eq]] -## (\template [<tag>] -## [[[_ (<tag> xs')] [_ (<tag> ys')]] -## (and (:: Int/Eq (E;= (size xs') (size ys'))) -## (foldL (lambda [old [x' y']] -## (and old (= x' y'))) -## true -## (zip2 xs' ys')))]) -## [[#;FormS] [#;TupleS]] + (\template [<tag>] + [[[_ (<tag> xs')] [_ (<tag> ys')]] + (and (:: Int/Eq (E;= (size xs') (size ys'))) + (foldL (lambda [old [x' y']] + (and old (= x' y'))) + true + ((zip 2) xs' ys')))]) + [[#;FormS] [#;TupleS]] -## [[_ (#;RecordS xs')] [_ (#;RecordS ys')]] -## (and (:: Int/Eq (E;= (size xs') (size ys'))) -## (foldL (lambda [old [[xl' xr'] [yl' yr']]] -## (and old (= xl' yl') (= xr' yr'))) -## true -## (zip2 xs' ys'))) + [[_ (#;RecordS xs')] [_ (#;RecordS ys')]] + (and (:: Int/Eq (E;= (size xs') (size ys'))) + (foldL (lambda [old [[xl' xr'] [yl' yr']]] + (and old (= xl' yl') (= xr' yr'))) + true + ((zip 2) xs' ys'))) -## _ -## false))) + _ + false))) diff --git a/source/lux/meta/lux.lux b/source/lux/meta/lux.lux index edf3a8667..66f1a554b 100644 --- a/source/lux/meta/lux.lux +++ b/source/lux/meta/lux.lux @@ -9,7 +9,7 @@ (functor #as F) (monad #as M #refer (#only do)) (show #as S)) - (lux/data list + (lux/data (list #refer #all #open ("list:" List/Monoid)) (text #as T #open ("text:" Text/Monoid Text/Eq)) (number/int #as I #open ("i" Int/Number)))) @@ -65,7 +65,7 @@ #;Nil #;None - (#;Cons [[k' v] plist']) + (#;Cons [k' v] plist') (if (text:= k k') (#;Some v) (get k plist')))) diff --git a/source/lux/meta/syntax.lux b/source/lux/meta/syntax.lux index 4ee3163b0..5425a2d9c 100644 --- a/source/lux/meta/syntax.lux +++ b/source/lux/meta/syntax.lux @@ -12,7 +12,7 @@ (data (bool #as b) (char #as c) (text #as t #open ("text:" Text/Monoid Text/Eq)) - list + (list #refer #all #open ("" List/Fold)) (number (int #open ("i" Int/Eq)) (real #open ("r" Real/Eq)))))) diff --git a/source/lux/meta/type.lux b/source/lux/meta/type.lux index d32ea993b..4147e37d4 100644 --- a/source/lux/meta/type.lux +++ b/source/lux/meta/type.lux @@ -13,6 +13,8 @@ (list #refer #all #open ("list:" List/Monad))) )) +(open List/Fold) + ## [Structures] (defstruct #export Type/Show (Show Type) (def (show type) @@ -61,46 +63,46 @@ ($ text:++ module ";" name) ))) -## (defstruct #export Type/Eq (Eq Type) -## (def (= x y) -## (case [x y] -## [(#;DataT xname) (#;DataT yname)] -## (text:= xname yname) - -## (\or [(#;VarT xid) (#;VarT yid)] -## [(#;ExT xid) (#;ExT yid)] -## [(#;BoundT xid) (#;BoundT yid)]) -## (int:= xid yid) - -## (\or [(#;LambdaT xleft xright) (#;LambdaT yleft yright)] -## [(#;AppT xleft xright) (#;AppT yleft yright)]) -## (and (= xleft yleft) -## (= xright yright)) - -## [(#;NamedT [xmodule xname] xtype) (#;NamedT [ymodule yname] ytype)] -## (and (text:= xmodule ymodule) -## (text:= xname yname) -## (= xtype ytype)) - -## (\or [(#;TupleT xmembers) (#;TupleT ymembers)] -## [(#;VariantT xmembers) (#;VariantT ymembers)]) -## (and (int:= (size xmembers) (size ymembers)) -## (foldL (lambda [prev [x y]] -## (and prev (= v y))) -## true -## (zip2 xmembers ymembers))) - -## (\or [(#;UnivQ yenv ybody) (#;UnivQ yenv ybody)] -## [(#;ExQ yenv ybody) (#;ExQ yenv ybody)]) -## (and (int:= (size xenv) (size yenv)) -## (foldL (lambda [prev [x y]] -## (and prev (= v y))) -## (= xbody ybody) -## (zip2 xenv yenv))) - -## _ -## false -## ))) +(defstruct #export Type/Eq (Eq Type) + (def (= x y) + (case [x y] + [(#;DataT xname) (#;DataT yname)] + (text:= xname yname) + + (\or [(#;VarT xid) (#;VarT yid)] + [(#;ExT xid) (#;ExT yid)] + [(#;BoundT xid) (#;BoundT yid)]) + (int:= xid yid) + + (\or [(#;LambdaT xleft xright) (#;LambdaT yleft yright)] + [(#;AppT xleft xright) (#;AppT yleft yright)]) + (and (= xleft yleft) + (= xright yright)) + + [(#;NamedT [xmodule xname] xtype) (#;NamedT [ymodule yname] ytype)] + (and (text:= xmodule ymodule) + (text:= xname yname) + (= xtype ytype)) + + (\or [(#;TupleT xmembers) (#;TupleT ymembers)] + [(#;VariantT xmembers) (#;VariantT ymembers)]) + (and (int:= (size xmembers) (size ymembers)) + (foldL (lambda [prev [x y]] + (and prev (= x y))) + true + ((zip 2) xmembers ymembers))) + + (\or [(#;UnivQ xenv xbody) (#;UnivQ yenv ybody)] + [(#;ExQ xenv xbody) (#;ExQ yenv ybody)]) + (and (int:= (size xenv) (size yenv)) + (foldL (lambda [prev [x y]] + (and prev (= x y))) + (= xbody ybody) + ((zip 2) xenv yenv))) + + _ + false + ))) ## [Functions] (def #export (beta-reduce env type) |