aboutsummaryrefslogtreecommitdiff
path: root/stdlib
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib')
-rw-r--r--stdlib/source/lux.lux63
-rw-r--r--stdlib/source/lux/data/coll/list.lux4
-rw-r--r--stdlib/source/lux/data/number.lux72
-rw-r--r--stdlib/source/lux/data/text.lux2
-rw-r--r--stdlib/source/lux/meta/type/auto.lux4
-rw-r--r--stdlib/source/lux/meta/type/check.lux109
-rw-r--r--stdlib/test/test/lux/meta/type/check.lux68
7 files changed, 114 insertions, 208 deletions
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<Maybe>
@@ -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 [<type>
- <=-proc> <lt-proc> <=-name> <lt-name> <lte-name> <gt-name> <gte-name>
+ <eq-proc> <lt-proc> <eq-name> <lt-name> <lte-name> <gt-name> <gte-name>
<eq-doc> <<-doc> <<=-doc> <>-doc> <>=-doc>]
- [(def:''' #export (<=-name> test subject)
+ [(def:''' #export (<eq-name> test subject)
(list [(tag$ ["lux" "doc"]) (text$ <eq-doc>)])
(-> <type> <type> Bool)
- (<=-proc> subject test))
+ (<eq-proc> subject test))
(def:''' #export (<lt-name> test subject)
(list [(tag$ ["lux" "doc"]) (text$ <<-doc>)])
@@ -2228,7 +2227,7 @@
(-> <type> <type> Bool)
(if (<lt-proc> subject test)
true
- (<=-proc> subject test)))
+ (<eq-proc> subject test)))
(def:''' #export (<gt-name> test subject)
(list [(tag$ ["lux" "doc"]) (text$ <>-doc>)])
@@ -2240,7 +2239,7 @@
(-> <type> <type> Bool)
(if (<lt-proc> test subject)
true
- (<=-proc> subject test)))]
+ (<eq-proc> 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<Maybe>
[bindings' (monad/map Monad<Maybe> get-name bindings)
data' (monad/map Monad<Maybe> 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 <char-set> (n.% <base> input)))
- output' ("lux text append" digit output)
+ output' ("lux text concat" digit output)
input' (n./ <base> 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" <char-set> digit +0)
#;None
- (#E;Error ("lux text append" <error> repr))
+ (#E;Error ("lux text concat" <error> repr))
(#;Some index)
(recur (n.inc idx)
@@ -208,8 +208,8 @@
(#E;Success output))))
_
- (#E;Error ("lux text append" <error> repr)))
- (#E;Error ("lux text append" <error> repr))))))]
+ (#E;Error ("lux text concat" <error> repr)))
+ (#E;Error ("lux text concat" <error> repr))))))]
[Binary@Codec<Text,Nat> +2 "01" "Invalid binary syntax for Nat: "]
[Octal@Codec<Text,Nat> +8 "01234567" "Invalid octal syntax for Nat: "]
@@ -230,10 +230,10 @@
(get-char <char-set>)
maybe;assume)]
(if (i.= 0 input)
- ("lux text append" sign output)
+ ("lux text concat" sign output)
(let [digit (maybe;assume (get-char <char-set> (int-to-nat (i.% <base> input))))]
(recur (i./ <base> 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 ".")))
- [(:: <nat> decode ("lux text append" "+" (de-prefix repr)))
+ [(:: <nat> decode ("lux text concat" "+" (de-prefix repr)))
(#;Some output)])
(#E;Success (:! Deg output))
_
- (#E;Error ("lux text append" <error> repr)))
- (#E;Error ("lux text append" <error> repr))))))]
+ (#E;Error ("lux text concat" <error> repr)))
+ (#E;Error ("lux text concat" <error> repr))))))]
[Binary@Codec<Text,Deg> Binary@Codec<Text,Nat> +1 "Invalid binary syntax: "]
[Octal@Codec<Text,Deg> Octal@Codec<Text,Nat> +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.* <base> dec-left)
digit (|> shifted (f.% <base>) frac-to-int int-to-nat
(get-char <char-set>) 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.* <base> output))))
adjusted-decimal (|> decimal int-to-frac (f./ div-power))
- dec-deg (case (:: Hex@Codec<Text,Deg> decode ("lux text append" "." decimal-part))
+ dec-deg (case (:: Hex@Codec<Text,Deg> 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" <error> repr))))
+ (#E;Error ("lux text concat" <error> repr))))
_
- (#E;Error ("lux text append" <error> repr)))))]
+ (#E;Error ("lux text concat" <error> repr)))))]
[Binary@Codec<Text,Frac> Binary@Codec<Text,Int> 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 [<from> <from-translator> <to> <to-translator> <base-bits>]
[(def: (<from> 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 <base-bits>)
(map <from-translator>)
@@ -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 (|> (<from> false decimal-part)
- ("lux text append" ".")
- ("lux text append" (<from> true whole-part))
- ("lux text append" (if (f.= -1.0 sign) "-" "")))]
+ ("lux text concat" ".")
+ ("lux text concat" (<from> 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 (|> (<to> decimal-part)
- ("lux text append" ".")
- ("lux text append" (<to> whole-part))
- ("lux text append" (if (f.= -1.0 sign) "-" "")))]
+ ("lux text concat" ".")
+ ("lux text concat" (<to> whole-part))
+ ("lux text concat" (if (f.= -1.0 sign) "-" "")))]
(case (:: Binary@Codec<Text,Frac> decode as-binary)
(#E;Error _)
- (#E;Error ("lux text append" <error> repr))
+ (#E;Error ("lux text concat" <error> repr))
output
output))
_
- (#E;Error ("lux text append" <error> repr))))))]
+ (#E;Error ("lux text concat" <error> repr))))))]
[Octal@Codec<Text,Frac> "Invalid octaladecimal syntax: " binary-to-octal octal-to-binary]
[Hex@Codec<Text,Frac> "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<Text,Int> 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> "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<Check>
- [[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<Check>
- [[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<Check>
- [? (bound? id)]
- (if ?
+ (do Monad<Check>
+ [? (concrete? id)]
+ (if ?
+ (if (n.= t-id id)
(read id)
- (wrap type)))
- (do Monad<Check>
- [? (concrete? id)]
- (if ?
(do Monad<Check>
[=type (read id)
==type (clean t-id =type)
_ (update ==type id)]
- (wrap type))
- (wrap type))))
+ (wrap type)))
+ (wrap type)))
(#;Primitive name params)
(do Monad<Check>
@@ -290,7 +275,7 @@
(:: Monad<Check> 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<Nat>))
@@ -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<Check>
- [_ (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<Check>
- [[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<Check>
- [actual' (apply-type! actual var)
- assumptions (check' expected actual' assumptions)
- _ (clean var-id expected)]
- (check/wrap assumptions))))
+ (do Monad<Check>
+ [[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<Check>
- [expected' (apply-type! expected var)
- assumptions (check' expected' actual assumptions)
- _ (clean var-id actual)]
- (check/wrap assumptions))))
+ (do Monad<Check>
+ [[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<Check>
diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux
index 21eed2f72..b1239fa43 100644
--- a/stdlib/test/test/lux/meta/type/check.lux
+++ b/stdlib/test/test/lux/meta/type/check.lux
@@ -159,36 +159,42 @@
(context: "Type-vars"
($_ seq
(test "Type-vars check against themselves."
- (type-checks? (@;with (function [[id var]] (@;check var var)))))
+ (type-checks? (do @;Monad<Check>
+ [[id var] @;var]
+ (@;check var var))))
(test "Can bind unbound type-vars by type-checking against them."
- (and (type-checks? (@;with (function [[id var]] (@;check var #;Unit))))
- (type-checks? (@;with (function [[id var]] (@;check #;Unit var))))))
+ (and (type-checks? (do @;Monad<Check>
+ [[id var] @;var]
+ (@;check var #;Unit)))
+ (type-checks? (do @;Monad<Check>
+ [[id var] @;var]
+ (@;check #;Unit var)))))
(test "Cannot rebind already bound type-vars."
- (not (type-checks? (@;with (function [[id var]]
- (do @;Monad<Check>
- [_ (@;check var #;Unit)]
- (@;check var #;Void)))))))
+ (not (type-checks? (do @;Monad<Check>
+ [[id var] @;var
+ _ (@;check var #;Unit)]
+ (@;check var #;Void)))))
(test "If the type bound to a var is a super-type to another, then the var is also a super-type."
- (type-checks? (@;with (function [[id var]]
- (do @;Monad<Check>
- [_ (@;check var Top)]
- (@;check var #;Unit))))))
+ (type-checks? (do @;Monad<Check>
+ [[id var] @;var
+ _ (@;check var Top)]
+ (@;check var #;Unit))))
(test "If the type bound to a var is a sub-type of another, then the var is also a sub-type."
- (type-checks? (@;with (function [[id var]]
- (do @;Monad<Check>
- [_ (@;check var Bottom)]
- (@;check #;Unit var))))))
+ (type-checks? (do @;Monad<Check>
+ [[id var] @;var
+ _ (@;check var Bottom)]
+ (@;check #;Unit var))))
))
(def: (build-ring num-connections)
(-> Nat (@;Check [[Nat Type] (List [Nat Type]) [Nat Type]]))
(do @;Monad<Check>
- [[head-id head-type] @;create
- ids+types (monad;seq @ (list;repeat num-connections @;create))
+ [[head-id head-type] @;var
+ ids+types (monad;seq @ (list;repeat num-connections @;var))
[tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]]
(do @
[_ (@;check head-type tail-type)]
@@ -234,34 +240,6 @@
(@;assert ""
(and rings-were-erased?
same-types?))))))
- (test "Can delete variables from rings."
- (type-checks? (do @;Monad<Check>
- [[[head-id head-type] ids+types [tail-id tail-type]] (build-ring num-connections)
- #let [ids (list/map product;left ids+types)
- all-ids (#;Cons head-id ids)
- num-all-ids (list;size all-ids)
- [_ idx] (r;run (r;pcg-32 pick-pcg)
- (|> r;nat (:: r;Monad<Random> map (n.% num-all-ids))))]
- #let [pick (maybe;assume (list;nth idx all-ids))]
- _ (@;delete pick)]
- (if (n.= +0 num-connections)
- (wrap [])
- (do @
- [ring (@;ring (if (n.= head-id pick)
- tail-id
- head-id))
- #let [without-removal (|> (list (list;take idx all-ids)
- (list;drop (n.inc idx) all-ids))
- list;concat
- (list;sort n.<))]]
- (let [missing-link? (n.= (n.dec num-all-ids) (set;size ring))
- ids-match? (|> (set;to-list ring)
- (list;sort n.<)
- (:: (list;Eq<List> number;Eq<Nat>) = without-removal))]
- (@;assert ""
- (and missing-link?
- ids-match?)))))
- )))
(test "Can merge multiple rings of variables."
(type-checks? (do @;Monad<Check>
[[[head-idL head-typeL] ids+typesL [tail-idL tail-typeL]] (build-ring num-connections)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-23 10:04:46 +0000