From 2a3946e713821880ecc47580e754315349f2fe73 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Mon, 13 Nov 2017 20:02:18 -0400 Subject: - Type-vars no longer get deleted. - Fixed some bugs. --- stdlib/source/lux.lux | 63 ++++++++++---------- stdlib/source/lux/data/coll/list.lux | 4 +- stdlib/source/lux/data/number.lux | 72 +++++++++++----------- stdlib/source/lux/data/text.lux | 2 +- stdlib/source/lux/meta/type/auto.lux | 4 +- stdlib/source/lux/meta/type/check.lux | 109 ++++++---------------------------- 6 files changed, 91 insertions(+), 163 deletions(-) (limited to 'stdlib/source') diff --git a/stdlib/source/lux.lux b/stdlib/source/lux.lux index 738183410..9b41010d9 100644 --- a/stdlib/source/lux.lux +++ b/stdlib/source/lux.lux @@ -1208,8 +1208,8 @@ (def:'' (length list) #;Nil (#UnivQ #Nil - (#Function ($' List (#Bound +1)) Int)) - (fold (function'' [_ acc] ("lux int +" 1 acc)) 0 list)) + (#Function ($' List (#Bound +1)) Nat)) + (fold (function'' [_ acc] ("lux nat +" +1 acc)) +0 list)) (macro:' #export (All tokens) (#Cons [(tag$ ["lux" "doc"]) @@ -1250,8 +1250,7 @@ [false _] (replace-syntax (#Cons [self-name (make-bound ("lux nat *" +2 ("lux nat -" - ("lux int to-nat" - (length names)) + (length names) +1)))] #Nil) body')}) @@ -1302,7 +1301,7 @@ [false _] (replace-syntax (#Cons [self-name (make-bound ("lux nat *" +2 ("lux nat -" - ("lux int to-nat" (length names)) + (length names) +1)))] #Nil) body')}) @@ -1634,8 +1633,8 @@ (#Named ["lux" "Monad"] (All [m] (& (All [a] (-> a ($' m a))) - (All [a b] (-> ($' m a) - (-> a ($' m b)) + (All [a b] (-> (-> a ($' m b)) + ($' m a) ($' m b))))))) (def:''' Monad @@ -1645,7 +1644,7 @@ (function' [x] (#Some x)) #bind - (function' [ma f] + (function' [f ma] ("lux case" ma {#None #None (#Some a) (f a)}))}) @@ -1659,7 +1658,7 @@ (#Right state x))) #bind - (function' [ma f] + (function' [f ma] (function' [state] ("lux case" (ma state) {(#Left msg) @@ -1682,8 +1681,8 @@ _ (form$ (list g!bind - value - (form$ (list (text$ "lux function") (symbol$ ["" ""]) var body'))))})))) + (form$ (list (text$ "lux function") (symbol$ ["" ""]) var body')) + value))})))) body (reverse (as-pairs bindings)))] (return (list (form$ (list (text$ "lux case") @@ -1770,7 +1769,7 @@ (def:''' (text/compose x y) #Nil (-> Text Text Text) - ("lux text append" x y)) + ("lux text concat" x y)) (def:''' (ident/encode ident) #Nil @@ -2197,7 +2196,7 @@ (let' [apply ("lux check" (-> RepEnv ($' List Code)) (function' [env] (map (apply-template env) templates))) num-bindings (length bindings')] - (if (every? (function' [sample] ("lux int =" num-bindings sample)) + (if (every? (function' [sample] ("lux nat =" num-bindings sample)) (map length data')) (|> data' (join-map (. apply (make-env bindings'))) @@ -2211,12 +2210,12 @@ (fail "Wrong syntax for do-template")})) (do-template [ - <=-proc> <=-name> + <<-doc> <<=-doc> <>-doc> <>=-doc>] - [(def:''' #export (<=-name> test subject) + [(def:''' #export ( test subject) (list [(tag$ ["lux" "doc"]) (text$ )]) (-> Bool) - (<=-proc> subject test)) + ( subject test)) (def:''' #export ( test subject) (list [(tag$ ["lux" "doc"]) (text$ <<-doc>)]) @@ -2228,7 +2227,7 @@ (-> Bool) (if ( subject test) true - (<=-proc> subject test))) + ( subject test))) (def:''' #export ( test subject) (list [(tag$ ["lux" "doc"]) (text$ <>-doc>)]) @@ -2240,7 +2239,7 @@ (-> Bool) (if ( test subject) true - (<=-proc> subject test)))] + ( subject test)))] [ Nat "lux nat =" "lux nat <" n.= n.< n.<= n.> n.>= "Nat(ural) equality." "Nat(ural) less-than." "Nat(ural) less-than-equal." "Nat(ural) greater-than." "Nat(ural) greater-than-equal."] @@ -2343,9 +2342,9 @@ (let' [loop ("lux check" (-> Nat Text Text) (function' recur [input output] (if ("lux nat =" input +0) - ("lux text append" "+" output) + ("lux text concat" "+" output) (recur ("lux nat /" input +10) - ("lux text append" (digit-to-text ("lux nat %" input +10)) + ("lux text concat" (digit-to-text ("lux nat %" input +10)) output)))))] (loop value ""))})) @@ -2367,9 +2366,9 @@ (("lux check" (-> Int Text Text) (function' recur [input output] (if (i.= 0 input) - ("lux text append" sign output) + ("lux text concat" sign output) (recur (i./ 10 input) - ("lux text append" (|> input (i.% 10) ("lux coerce" Nat) digit-to-text) + ("lux text concat" (|> input (i.% 10) ("lux coerce" Nat) digit-to-text) output))))) (|> value (i./ 10) int/abs) (|> value (i.% 10) int/abs ("lux coerce" Nat) digit-to-text))))) @@ -2381,8 +2380,8 @@ (def:''' (multiple? div n) #Nil - (-> Int Int Bool) - (i.= 0 (i.% div n))) + (-> Nat Nat Bool) + (|> n (n.% div) (n.= +0))) (def:''' #export (not x) (list [(tag$ ["lux" "doc"]) @@ -2982,7 +2981,7 @@ (op x y))")]) (case tokens (^ (list [_ (#Tuple bindings)] body)) - (if (multiple? 2 (length bindings)) + (if (multiple? +2 (length bindings)) (|> bindings as-pairs reverse (fold (: (-> [Code Code] Code Code) (function' [lr body'] @@ -3436,15 +3435,15 @@ (def: (nth idx xs) (All [a] - (-> Int (List a) (Maybe a))) + (-> Nat (List a) (Maybe a))) (case xs #Nil #None (#Cons x xs') - (if (i.= idx 0) + (if (n.= +0 idx) (#Some x) - (nth (i.- 1 idx) xs') + (nth (n.- +1 idx) xs') ))) (def: (beta-reduce env type) @@ -3479,7 +3478,7 @@ (#Function (beta-reduce env ?input) (beta-reduce env ?output)) (#Bound idx) - (case (nth ("lux nat to-int" idx) env) + (case (nth idx env) (#Some bound) bound @@ -4073,7 +4072,7 @@ parts (let [[ups parts'] (split-with (text/= "..") parts) num-ups (length ups)] - (if (i.= num-ups 0) + (if (n.= +0 num-ups) (return module) (case (nth num-ups (split-module-contexts current-module)) #None @@ -4433,7 +4432,7 @@ (n.odd? num) \"odd\" ## else-branch \"???\")"} - (if (i.= 0 (i.% 2 (length tokens))) + (if (n.= +0 (n.% +2 (length tokens))) (fail "cond requires an even number of arguments.") (case (reverse tokens) (^ (list& else branches')) @@ -4971,7 +4970,7 @@ (do Monad [bindings' (monad/map Monad get-name bindings) data' (monad/map Monad tuple->list data)] - (if (every? (i.= (length bindings')) (map length data')) + (if (every? (n.= (length bindings')) (map length data')) (let [apply (: (-> RepEnv (List Code)) (function [env] (map (apply-template env) templates)))] (|> data' diff --git a/stdlib/source/lux/data/coll/list.lux b/stdlib/source/lux/data/coll/list.lux index efdb727a5..4d4090835 100644 --- a/stdlib/source/lux/data/coll/list.lux +++ b/stdlib/source/lux/data/coll/list.lux @@ -368,7 +368,7 @@ (map (function [idx] (let [base (Nat/encode idx)] [(symbol$ base) - (symbol$ ("lux text append" base "'"))])))) + (symbol$ ("lux text concat" base "'"))])))) pattern (` [(~@ (map (function [[v vs]] (` (#;Cons (~ v) (~ vs)))) vars+lists))]) g!step (symbol$ "\tstep\t") @@ -415,7 +415,7 @@ (map (function [idx] (let [base (Nat/encode idx)] [(symbol$ base) - (symbol$ ("lux text append" base "'"))])))) + (symbol$ ("lux text concat" base "'"))])))) pattern (` [(~@ (map (function [[v vs]] (` (#;Cons (~ v) (~ vs)))) vars+lists))]) g!step (symbol$ "\tstep\t") diff --git a/stdlib/source/lux/data/number.lux b/stdlib/source/lux/data/number.lux index 4dc0e4685..e9009102b 100644 --- a/stdlib/source/lux/data/number.lux +++ b/stdlib/source/lux/data/number.lux @@ -182,10 +182,10 @@ (loop [input value output ""] (let [digit (maybe;assume (get-char (n.% input))) - output' ("lux text append" digit output) + output' ("lux text concat" digit output) input' (n./ input)] (if (n.= +0 input') - ("lux text append" "+" output') + ("lux text concat" "+" output') (recur input' output'))))) (def: (decode repr) @@ -200,7 +200,7 @@ (let [digit (maybe;assume (get-char input idx))] (case ("lux text index" digit +0) #;None - (#E;Error ("lux text append" repr)) + (#E;Error ("lux text concat" repr)) (#;Some index) (recur (n.inc idx) @@ -208,8 +208,8 @@ (#E;Success output)))) _ - (#E;Error ("lux text append" repr))) - (#E;Error ("lux text append" repr))))))] + (#E;Error ("lux text concat" repr))) + (#E;Error ("lux text concat" repr))))))] [Binary@Codec +2 "01" "Invalid binary syntax for Nat: "] [Octal@Codec +8 "01234567" "Invalid octal syntax for Nat: "] @@ -230,10 +230,10 @@ (get-char ) maybe;assume)] (if (i.= 0 input) - ("lux text append" sign output) + ("lux text concat" sign output) (let [digit (maybe;assume (get-char (int-to-nat (i.% input))))] (recur (i./ input) - ("lux text append" digit output)))))))) + ("lux text concat" digit output)))))))) (def: (decode repr) (let [input-size ("lux text size" repr)] @@ -280,22 +280,22 @@ (if (n.= +0 zeroes-left) output (recur (n.dec zeroes-left) - ("lux text append" "0" output)))) - padded-output ("lux text append" zero-padding raw-output)] - ("lux text append" "." padded-output))) + ("lux text concat" "0" output)))) + padded-output ("lux text concat" zero-padding raw-output)] + ("lux text concat" "." padded-output))) (def: (decode repr) (let [repr-size ("lux text size" repr)] (if (n.>= +2 repr-size) (case ("lux text char" repr +0) (^multi (^ (#;Some (char "."))) - [(:: decode ("lux text append" "+" (de-prefix repr))) + [(:: decode ("lux text concat" "+" (de-prefix repr))) (#;Some output)]) (#E;Success (:! Deg output)) _ - (#E;Error ("lux text append" repr))) - (#E;Error ("lux text append" repr))))))] + (#E;Error ("lux text concat" repr))) + (#E;Error ("lux text concat" repr))))))] [Binary@Codec Binary@Codec +1 "Invalid binary syntax: "] [Octal@Codec Octal@Codec +3 "Invalid octal syntax: "] @@ -313,13 +313,13 @@ (loop [dec-left decimal output ""] (if (f.= 0.0 dec-left) - ("lux text append" "." output) + ("lux text concat" "." output) (let [shifted (f.* dec-left) digit (|> shifted (f.% ) frac-to-int int-to-nat (get-char ) maybe;assume)] (recur (f.% 1.0 shifted) - ("lux text append" output digit))))))] - ("lux text append" whole-part decimal-part))) + ("lux text concat" output digit))))))] + ("lux text concat" whole-part decimal-part))) (def: (decode repr) (case ("lux text index" repr "." +0) @@ -340,7 +340,7 @@ (recur (n.dec muls-left) (f.* output)))) adjusted-decimal (|> decimal int-to-frac (f./ div-power)) - dec-deg (case (:: Hex@Codec decode ("lux text append" "." decimal-part)) + dec-deg (case (:: Hex@Codec decode ("lux text concat" "." decimal-part)) (#E;Success dec-deg) dec-deg @@ -350,10 +350,10 @@ (f.* sign adjusted-decimal)))) _ - (#E;Error ("lux text append" repr)))) + (#E;Error ("lux text concat" repr)))) _ - (#E;Error ("lux text append" repr)))))] + (#E;Error ("lux text concat" repr)))))] [Binary@Codec Binary@Codec 2.0 "01" "Invalid binary syntax: "] ) @@ -457,7 +457,7 @@ "" (#;Cons x xs') - ("lux text append" x (re-join-chunks xs')))) + ("lux text concat" x (re-join-chunks xs')))) (do-template [ ] [(def: ( on-left? input) @@ -473,10 +473,10 @@ (if (n.= +0 zeroes-left) output (recur (n.dec zeroes-left) - ("lux text append" "0" output)))))) + ("lux text concat" "0" output)))))) padded-input (if on-left? - ("lux text append" zero-padding input) - ("lux text append" input zero-padding))] + ("lux text concat" zero-padding input) + ("lux text concat" input zero-padding))] (|> padded-input (segment-digits ) (map ) @@ -504,9 +504,9 @@ dot-idx)) decimal-part (maybe;assume ("lux text clip" raw-bin (n.inc dot-idx) ("lux text size" raw-bin))) hex-output (|> ( false decimal-part) - ("lux text append" ".") - ("lux text append" ( true whole-part)) - ("lux text append" (if (f.= -1.0 sign) "-" "")))] + ("lux text concat" ".") + ("lux text concat" ( true whole-part)) + ("lux text concat" (if (f.= -1.0 sign) "-" "")))] hex-output)) (def: (decode repr) @@ -521,18 +521,18 @@ (let [whole-part (maybe;assume ("lux text clip" repr (if (f.= -1.0 sign) +1 +0) split-index)) decimal-part (maybe;assume ("lux text clip" repr (n.inc split-index) ("lux text size" repr))) as-binary (|> ( decimal-part) - ("lux text append" ".") - ("lux text append" ( whole-part)) - ("lux text append" (if (f.= -1.0 sign) "-" "")))] + ("lux text concat" ".") + ("lux text concat" ( whole-part)) + ("lux text concat" (if (f.= -1.0 sign) "-" "")))] (case (:: Binary@Codec decode as-binary) (#E;Error _) - (#E;Error ("lux text append" repr)) + (#E;Error ("lux text concat" repr)) output output)) _ - (#E;Error ("lux text append" repr))))))] + (#E;Error ("lux text concat" repr))))))] [Octal@Codec "Invalid octaladecimal syntax: " binary-to-octal octal-to-binary] [Hex@Codec "Invalid hexadecimal syntax: " binary-to-hex hex-to-binary] @@ -605,7 +605,7 @@ (def: (prepend left right) (-> Text Text Text) - ("lux text append" left right)) + ("lux text concat" left right)) (def: (digits-times-5! idx output) (-> Nat Digits Digits) @@ -643,7 +643,7 @@ (recur (n.dec idx) true output) (recur (n.dec idx) false - ("lux text append" + ("lux text concat" (:: Codec encode (:! Int digit)) output)))) (if all-zeroes? @@ -730,7 +730,7 @@ digits')) (recur (n.dec idx) digits)) - ("lux text append" "." (digits-to-text digits)) + ("lux text concat" "." (digits-to-text digits)) ))))) (def: (decode input) @@ -761,8 +761,8 @@ (#E;Success (:! Deg output)))) #;None - (#E;Error ("lux text append" "Wrong syntax for Deg: " input))) - (#E;Error ("lux text append" "Wrong syntax for Deg: " input)))) + (#E;Error ("lux text concat" "Wrong syntax for Deg: " input))) + (#E;Error ("lux text concat" "Wrong syntax for Deg: " input)))) )) (def: (log2 input) diff --git a/stdlib/source/lux/data/text.lux b/stdlib/source/lux/data/text.lux index e8eb20b43..812047e35 100644 --- a/stdlib/source/lux/data/text.lux +++ b/stdlib/source/lux/data/text.lux @@ -131,7 +131,7 @@ (struct: #export _ (Monoid Text) (def: identity "") (def: (compose left right) - ("lux text append" left right))) + ("lux text concat" left right))) (open Monoid "text/") diff --git a/stdlib/source/lux/meta/type/auto.lux b/stdlib/source/lux/meta/type/auto.lux index 0162d7a04..a2013d3b1 100644 --- a/stdlib/source/lux/meta/type/auto.lux +++ b/stdlib/source/lux/meta/type/auto.lux @@ -156,7 +156,7 @@ (#;UnivQ _) (do Monad - [[id var] tc;create] + [[id var] tc;var] (apply-function-type (maybe;assume (type;apply (list var) func)) arg)) @@ -173,7 +173,7 @@ (case type (#;UnivQ _) (do Monad - [[id var] tc;create + [[id var] tc;var [ids final-output] (concrete-type (maybe;assume (type;apply (list var) type)))] (wrap [(#;Cons id ids) final-output])) diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux index b12470418..bd49a5588 100644 --- a/stdlib/source/lux/meta/type/check.lux +++ b/stdlib/source/lux/meta/type/check.lux @@ -230,36 +230,21 @@ #;None (ex;throw Unknown-Type-Var (nat/encode id))))) -(def: #export (clear id) - (-> Var (Check Unit)) - (function [context] - (case (|> context (get@ #;var-bindings) (var::get id)) - (#;Some _) - (#e;Success [(update@ #;var-bindings (var::put id #;None) context) - []]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode id))))) - (def: #export (clean t-id type) (-> Var Type (Check Type)) (case type (#;Var id) - (if (n.= t-id id) - (do Monad - [? (bound? id)] - (if ? + (do Monad + [? (concrete? id)] + (if ? + (if (n.= t-id id) (read id) - (wrap type))) - (do Monad - [? (concrete? id)] - (if ? (do Monad [=type (read id) ==type (clean t-id =type) _ (update ==type id)] - (wrap type)) - (wrap type)))) + (wrap type))) + (wrap type))) (#;Primitive name params) (do Monad @@ -290,7 +275,7 @@ (:: Monad wrap type) )) -(def: #export create +(def: #export var (Check [Var Type]) (function [context] (let [id (get@ #;var-counter context)] @@ -311,29 +296,6 @@ (#e;Success [(set@ #;var-bindings value context) []]))) -(def: (pre-link id) - (-> Var (Check (Maybe Var))) - (function [context] - (loop [current id] - (case (|> context (get@ #;var-bindings) (var::get current)) - (#;Some (#;Some type)) - (case type - (#;Var post) - (if (n.= id post) - (#e;Success [context (#;Some current)]) - (recur post)) - - _ - (if (n.= current id) - (#e;Success [context #;None]) - (ex;throw Improper-Ring (nat/encode id)))) - - (#;Some #;None) - (#e;Success [context #;None]) - - #;None - (ex;throw Unknown-Type-Var (nat/encode current)))))) - (type: #export Ring (Set Var)) (def: empty-ring Ring (set;new number;Hash)) @@ -360,37 +322,6 @@ #;None (ex;throw Unknown-Type-Var (nat/encode current)))))) -(def: (delete' id) - (-> Var (Check Unit)) - (function [context] - (#e;Success [(update@ #;var-bindings (var::remove id) context) - []]))) - -(def: #export (delete id) - (-> Var (Check Unit)) - (do Monad - [_ (wrap []) - ?link (pre-link id)] - (case ?link - #;None - (delete' id) - - (#;Some pre) - (do @ - [post (read id) - _ (if (type/= (#;Var pre) post) - (clear pre) - (update post pre))] - (delete' id))))) - -(def: #export (with k) - (All [a] (-> (-> [Var Type] (Check a)) (Check a))) - (do Monad - [[id var] create - output (k [id var]) - _ (delete id)] - (wrap output))) - (def: #export fresh-context Type-Context {#;var-counter +0 @@ -653,22 +584,20 @@ (check' expected' actual assumptions)) [_ (#;UnivQ _)] - (with - (function [[var-id var]] - (do Monad - [actual' (apply-type! actual var) - assumptions (check' expected actual' assumptions) - _ (clean var-id expected)] - (check/wrap assumptions)))) + (do Monad + [[var-id var] ;;var + actual' (apply-type! actual var) + assumptions (check' expected actual' assumptions) + _ (clean var-id expected)] + (check/wrap assumptions)) [(#;ExQ e!env e!def) _] - (with - (function [[var-id var]] - (do Monad - [expected' (apply-type! expected var) - assumptions (check' expected' actual assumptions) - _ (clean var-id actual)] - (check/wrap assumptions)))) + (do Monad + [[var-id var] ;;var + expected' (apply-type! expected var) + assumptions (check' expected' actual assumptions) + _ (clean var-id actual)] + (check/wrap assumptions)) [_ (#;ExQ a!env a!def)] (do Monad -- cgit v1.2.3