aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorEduardo Julian2017-11-13 20:02:18 -0400
committerEduardo Julian2017-11-13 20:02:18 -0400
commit2a3946e713821880ecc47580e754315349f2fe73 (patch)
tree7c32a522dff9d09293a5265baa968bc04137c944
parentca297162d5416a8c7b8af5f27757900d82d3ad03 (diff)
- Type-vars no longer get deleted.
- Fixed some bugs.
Diffstat (limited to '')
-rw-r--r--luxc/src/lux/analyser/proc/common.clj4
-rw-r--r--luxc/src/lux/compiler/js/proc/common.clj4
-rw-r--r--luxc/src/lux/compiler/jvm/proc/common.clj4
-rw-r--r--new-luxc/source/luxc/base.lux12
-rw-r--r--new-luxc/source/luxc/lang/analysis/case.lux2
-rw-r--r--new-luxc/source/luxc/lang/analysis/common.lux25
-rw-r--r--new-luxc/source/luxc/lang/analysis/function.lux5
-rw-r--r--new-luxc/source/luxc/lang/analysis/inference.lux12
-rw-r--r--new-luxc/source/luxc/lang/analysis/structure.lux18
-rw-r--r--new-luxc/source/luxc/lang/analysis/type.lux12
-rw-r--r--new-luxc/source/luxc/lang/translation.lux35
-rw-r--r--new-luxc/source/luxc/lang/translation/expression.jvm.lux2
-rw-r--r--new-luxc/source/luxc/lang/translation/function.jvm.lux67
-rw-r--r--new-luxc/source/luxc/lang/translation/reference.jvm.lux22
-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
21 files changed, 230 insertions, 316 deletions
diff --git a/luxc/src/lux/analyser/proc/common.clj b/luxc/src/lux/analyser/proc/common.clj
index 871dec4b3..182c08d63 100644
--- a/luxc/src/lux/analyser/proc/common.clj
+++ b/luxc/src/lux/analyser/proc/common.clj
@@ -41,7 +41,7 @@
^:private analyse-text-eq ["text" "="] &type/Text &type/Bool
^:private analyse-text-lt ["text" "<"] &type/Text &type/Bool
- ^:private analyse-text-append ["text" "append"] &type/Text &type/Text
+ ^:private analyse-text-concat ["text" "concat"] &type/Text &type/Text
)
(do-template [<name> <proc-name> <output-type>]
@@ -486,7 +486,7 @@
"lux text =" (analyse-text-eq analyse exo-type ?values)
"lux text <" (analyse-text-lt analyse exo-type ?values)
- "lux text append" (analyse-text-append analyse exo-type ?values)
+ "lux text concat" (analyse-text-concat analyse exo-type ?values)
"lux text clip" (analyse-text-clip analyse exo-type ?values)
"lux text index" (analyse-text-index analyse exo-type ?values)
"lux text last-index" (analyse-text-last-index analyse exo-type ?values)
diff --git a/luxc/src/lux/compiler/js/proc/common.clj b/luxc/src/lux/compiler/js/proc/common.clj
index a45bc2993..af4ff99e9 100644
--- a/luxc/src/lux/compiler/js/proc/common.clj
+++ b/luxc/src/lux/compiler/js/proc/common.clj
@@ -230,7 +230,7 @@
^:private compile-char-lt "<"
)
-(defn ^:private compile-text-append [compile ?values special-args]
+(defn ^:private compile-text-concat [compile ?values special-args]
(|do [:let [(&/$Cons ?x (&/$Cons ?y (&/$Nil))) ?values]
=x (compile ?x)
=y (compile ?y)]
@@ -446,7 +446,7 @@
(case proc
"=" (compile-text-eq compile ?values special-args)
"<" (compile-text-lt compile ?values special-args)
- "append" (compile-text-append compile ?values special-args)
+ "concat" (compile-text-concat compile ?values special-args)
"clip" (compile-text-clip compile ?values special-args)
"index" (compile-text-index compile ?values special-args)
"last-index" (compile-text-last-index compile ?values special-args)
diff --git a/luxc/src/lux/compiler/jvm/proc/common.clj b/luxc/src/lux/compiler/jvm/proc/common.clj
index 757f66afd..d7821e9af 100644
--- a/luxc/src/lux/compiler/jvm/proc/common.clj
+++ b/luxc/src/lux/compiler/jvm/proc/common.clj
@@ -484,7 +484,7 @@
(.visitLabel $end))]]
(return nil)))
-(defn compile-text-append [compile ?values special-args]
+(defn compile-text-concat [compile ?values special-args]
(|do [:let [(&/$Cons ?x (&/$Cons ?y (&/$Nil))) ?values]
^MethodVisitor *writer* &/get-writer
_ (compile ?x)
@@ -825,7 +825,7 @@
(case proc
"=" (compile-text-eq compile ?values special-args)
"<" (compile-text-lt compile ?values special-args)
- "append" (compile-text-append compile ?values special-args)
+ "concat" (compile-text-concat compile ?values special-args)
"clip" (compile-text-clip compile ?values special-args)
"index" (compile-text-index compile ?values special-args)
"last-index" (compile-text-last-index compile ?values special-args)
diff --git a/new-luxc/source/luxc/base.lux b/new-luxc/source/luxc/base.lux
index 580f5593f..c7768cd8c 100644
--- a/new-luxc/source/luxc/base.lux
+++ b/new-luxc/source/luxc/base.lux
@@ -63,6 +63,18 @@
(#e;Success [(set@ #;type-context context' compiler)
output]))))
+(def: #export (with-fresh-type-env action)
+ (All [a] (-> (Meta a) (Meta a)))
+ (function [compiler]
+ (let [old (get@ #;type-context compiler)]
+ (case (action (set@ #;type-context tc;fresh-context compiler))
+ (#e;Success [compiler' output])
+ (#e;Success [(set@ #;type-context old compiler')
+ output])
+
+ output
+ output))))
+
(def: #export (infer actualT)
(-> Type (Meta Unit))
(do meta;Monad<Meta>
diff --git a/new-luxc/source/luxc/lang/analysis/case.lux b/new-luxc/source/luxc/lang/analysis/case.lux
index f68733d7f..5f8ed344f 100644
--- a/new-luxc/source/luxc/lang/analysis/case.lux
+++ b/new-luxc/source/luxc/lang/analysis/case.lux
@@ -46,7 +46,7 @@
(#;Var id)
(do meta;Monad<Meta>
[? (&;with-type-env
- (tc;bound? id))]
+ (tc;concrete? id))]
(if ?
(do @
[type' (&;with-type-env
diff --git a/new-luxc/source/luxc/lang/analysis/common.lux b/new-luxc/source/luxc/lang/analysis/common.lux
index 4cbf5aedf..4d16e4ae6 100644
--- a/new-luxc/source/luxc/lang/analysis/common.lux
+++ b/new-luxc/source/luxc/lang/analysis/common.lux
@@ -1,7 +1,7 @@
(;module:
lux
(lux (control monad
- pipe)
+ ["ex" exception #+ exception:])
(data text/format
[product])
[meta #+ Monad<Meta>]
@@ -14,28 +14,25 @@
(All [a] (-> (Meta Analysis) (Meta [Type Analysis])))
(do Monad<Meta>
[[var-id var-type] (&;with-type-env
- tc;create)
+ tc;var)
analysis (&;with-expected-type var-type
action)
analysis-type (&;with-type-env
- (tc;clean var-id var-type))
- _ (&;with-type-env
- (tc;delete var-id))]
+ (tc;clean var-id var-type))]
(wrap [analysis-type analysis])))
(def: #export (with-var body)
(All [a] (-> (-> [Nat Type] (Meta a)) (Meta a)))
(do Monad<Meta>
[[id var] (&;with-type-env
- tc;create)
- output (body [id var])
- _ (&;with-type-env
- (tc;delete id))]
- (wrap output)))
+ tc;var)]
+ (body [id var])))
+
+(exception: #export Variant-Tag-Out-Of-Bounds)
(def: #export (variant-out-of-bounds-error type size tag)
(All [a] (-> Type Nat Nat (Meta a)))
- (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n"
- " Tag: " (%i (nat-to-int tag)) "\n"
- "Size: " (%i (nat-to-int size)) "\n"
- "Type: " (%type type))))
+ (&;throw Variant-Tag-Out-Of-Bounds
+ (format " Tag: " (%n tag) "\n"
+ "Variant Size: " (%n size) "\n"
+ "Variant Type: " (%type type))))
diff --git a/new-luxc/source/luxc/lang/analysis/function.lux b/new-luxc/source/luxc/lang/analysis/function.lux
index 5a6df4d3e..42a021577 100644
--- a/new-luxc/source/luxc/lang/analysis/function.lux
+++ b/new-luxc/source/luxc/lang/analysis/function.lux
@@ -108,8 +108,5 @@
(format "\n " (%n idx) " " (%code argC))))
(text;join-with "")))))
(do meta;Monad<Meta>
- [expectedT meta;expected-type
- [applyT argsA] (&inference;apply-function analyse funcT args)
- _ (&;with-type-env
- (tc;check expectedT applyT))]
+ [[applyT argsA] (&inference;apply-function analyse funcT args)]
(wrap (la;apply argsA funcA)))))
diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux
index fea685024..e2866ac87 100644
--- a/new-luxc/source/luxc/lang/analysis/inference.lux
+++ b/new-luxc/source/luxc/lang/analysis/inference.lux
@@ -99,7 +99,9 @@
(-> &;Analyser Type (List Code) (Meta [Type (List Analysis)]))
(case args
#;Nil
- (:: Monad<Meta> wrap [inferT (list)])
+ (do Monad<Meta>
+ [_ (&;infer inferT)]
+ (wrap [inferT (list)]))
(#;Cons argC args')
(case inferT
@@ -113,7 +115,7 @@
[[outputT argsA] (apply-function analyse (maybe;assume (type;apply (list varT) inferT)) args)]
(do @
[? (&;with-type-env
- (tc;bound? var-id))
+ (tc;concrete? var-id))
## Quantify over the type if genericity/parametricity
## is discovered.
outputT' (if ?
@@ -145,13 +147,13 @@
## things together more easily.
(#;Function inputT outputT)
(do Monad<Meta>
- [argA (&;with-stacked-errors
+ [[outputT' args'A] (apply-function analyse outputT args')
+ argA (&;with-stacked-errors
(function [_] (Cannot-Infer-Argument
(format "Inferred Type: " (%type inputT) "\n"
" Argument: " (%code argC))))
(&;with-expected-type inputT
- (analyse argC)))
- [outputT' args'A] (apply-function analyse outputT args')]
+ (analyse argC)))]
(wrap [outputT' (list& argA args'A)]))
_
diff --git a/new-luxc/source/luxc/lang/analysis/structure.lux b/new-luxc/source/luxc/lang/analysis/structure.lux
index 5cac1a0d3..9308fcfef 100644
--- a/new-luxc/source/luxc/lang/analysis/structure.lux
+++ b/new-luxc/source/luxc/lang/analysis/structure.lux
@@ -64,9 +64,9 @@
(#;Var id)
(do @
- [bound? (&;with-type-env
- (tc;bound? id))]
- (if bound?
+ [concrete? (&;with-type-env
+ (tc;concrete? id))]
+ (if concrete?
(do @
[expectedT' (&;with-type-env
(tc;read id))]
@@ -171,9 +171,9 @@
(#;Var id)
(do @
- [bound? (&;with-type-env
- (tc;bound? id))]
- (if bound?
+ [concrete? (&;with-type-env
+ (tc;concrete? id))]
+ (if concrete?
(do @
[expectedT' (&;with-type-env
(tc;read id))]
@@ -227,8 +227,6 @@
[#let [case-size (list;size group)]
inferenceT (&inference;variant idx case-size variantT)
[inferredT valueA+] (&inference;apply-function analyse inferenceT (list valueC))
- _ (&;with-type-env
- (tc;check expectedT inferredT))
temp &scope;next-local]
(wrap (la;sum idx case-size temp (|> valueA+ list;head maybe;assume))))
@@ -308,9 +306,7 @@
(#;Var _)
(do @
[inferenceT (&inference;record recordT)
- [inferredT membersA] (&inference;apply-function analyse inferenceT membersC)
- _ (&;with-type-env
- (tc;check expectedT inferredT))]
+ [inferredT membersA] (&inference;apply-function analyse inferenceT membersC)]
(wrap (la;product membersA)))
_
diff --git a/new-luxc/source/luxc/lang/analysis/type.lux b/new-luxc/source/luxc/lang/analysis/type.lux
index 74bb712f4..0a8abd76b 100644
--- a/new-luxc/source/luxc/lang/analysis/type.lux
+++ b/new-luxc/source/luxc/lang/analysis/type.lux
@@ -1,8 +1,8 @@
(;module:
lux
(lux (control monad)
- [meta #+ Monad<Meta>]
- (meta (type ["TC" check])))
+ [meta]
+ (meta (type ["tc" check])))
(luxc ["&" base]
(lang ["la" analysis #+ Analysis])))
@@ -11,21 +11,21 @@
## computing Lux type values.
(def: #export (analyse-check analyse eval type value)
(-> &;Analyser &;Eval Code Code (Meta Analysis))
- (do Monad<Meta>
+ (do meta;Monad<Meta>
[actualT (eval Type type)
#let [actualT (:! Type actualT)]
expectedT meta;expected-type
_ (&;with-type-env
- (TC;check expectedT actualT))]
+ (tc;check expectedT actualT))]
(&;with-expected-type actualT
(analyse value))))
(def: #export (analyse-coerce analyse eval type value)
(-> &;Analyser &;Eval Code Code (Meta Analysis))
- (do Monad<Meta>
+ (do meta;Monad<Meta>
[actualT (eval Type type)
expectedT meta;expected-type
_ (&;with-type-env
- (TC;check expectedT (:! Type actualT)))]
+ (tc;check expectedT (:! Type actualT)))]
(&;with-expected-type Top
(analyse value))))
diff --git a/new-luxc/source/luxc/lang/translation.lux b/new-luxc/source/luxc/lang/translation.lux
index 779cb92fd..c4ebf3642 100644
--- a/new-luxc/source/luxc/lang/translation.lux
+++ b/new-luxc/source/luxc/lang/translation.lux
@@ -39,24 +39,25 @@
(case code
(^code ("lux def" (~ [_ (#;Symbol ["" def-name])]) (~ valueC) (~ metaC)))
(hostL;with-context def-name
- (do meta;Monad<Meta>
- [[_ metaA] (&;with-scope
- (&;with-expected-type Code
- (analyse metaC)))
- metaI (expressionT;translate (expressionS;synthesize metaA))
- metaV (evalT;eval metaI)
- [_ valueT valueA] (&;with-scope
- (if (meta;type? (:! Code metaV))
- (&;with-expected-type Type
+ (&;with-fresh-type-env
+ (do meta;Monad<Meta>
+ [[_ metaA] (&;with-scope
+ (&;with-expected-type Code
+ (analyse metaC)))
+ metaI (expressionT;translate (expressionS;synthesize metaA))
+ metaV (evalT;eval metaI)
+ [_ valueT valueA] (&;with-scope
+ (if (meta;type? (:! Code metaV))
(do @
- [valueA (analyse valueC)]
- (wrap [Type valueA])))
- (commonA;with-unknown-type
- (analyse valueC))))
- valueI (expressionT;translate (expressionS;synthesize valueA))
- _ (&;with-scope
- (statementT;translate-def def-name valueT valueI metaI (:! Code metaV)))]
- (wrap [])))
+ [valueA (&;with-expected-type Type
+ (analyse valueC))]
+ (wrap [Type valueA]))
+ (commonA;with-unknown-type
+ (analyse valueC))))
+ valueI (expressionT;translate (expressionS;synthesize valueA))
+ _ (&;with-scope
+ (statementT;translate-def def-name valueT valueI metaI (:! Code metaV)))]
+ (wrap []))))
(^code ("lux program" (~ [_ (#;Symbol ["" program-args])]) (~ programC)))
(do meta;Monad<Meta>
diff --git a/new-luxc/source/luxc/lang/translation/expression.jvm.lux b/new-luxc/source/luxc/lang/translation/expression.jvm.lux
index 81cdc1261..fa5f54647 100644
--- a/new-luxc/source/luxc/lang/translation/expression.jvm.lux
+++ b/new-luxc/source/luxc/lang/translation/expression.jvm.lux
@@ -50,7 +50,7 @@
(^ [_ (#;Form (list [_ (#;Int var)]))])
(if (variableL;captured? var)
(referenceT;translate-captured var)
- (referenceT;translate-variable var))
+ (referenceT;translate-local var))
[_ (#;Symbol definition)]
(referenceT;translate-definition definition)
diff --git a/new-luxc/source/luxc/lang/translation/function.jvm.lux b/new-luxc/source/luxc/lang/translation/function.jvm.lux
index bbf295d18..ea6d371fa 100644
--- a/new-luxc/source/luxc/lang/translation/function.jvm.lux
+++ b/new-luxc/source/luxc/lang/translation/function.jvm.lux
@@ -14,22 +14,14 @@
(lang ["la" analysis]
["ls" synthesis]
(translation [";T" common]
- [";T" runtime])
+ [";T" runtime]
+ [";T" reference])
[";L" variable #+ Variable])))
(def: arity-field Text "arity")
(def: $Object $;Type ($t;class "java.lang.Object" (list)))
-(do-template [<name> <prefix>]
- [(def: #export (<name> idx)
- (-> Nat Text)
- (|> idx nat-to-int %i (format <prefix>)))]
-
- [captured "c"]
- [partial "p"]
- )
-
(def: (poly-arg? arity)
(-> ls;Arity Bool)
(n.> +1 arity))
@@ -97,7 +89,7 @@
(-> (List Variable) $;Def)
(|> (list;enumerate env)
(list/map (function [[env-idx env-source]]
- ($d;field #$;Private $;finalF (captured env-idx) $Object)))
+ ($d;field #$;Private $;finalF (referenceT;captured env-idx) $Object)))
$d;fuse))
(def: (with-partial arity)
@@ -105,28 +97,24 @@
(if (poly-arg? arity)
(|> (list;n.range +0 (n.- +2 arity))
(list/map (function [idx]
- ($d;field #$;Private $;finalF (partial idx) $Object)))
+ ($d;field #$;Private $;finalF (referenceT;partial idx) $Object)))
$d;fuse)
id))
(def: (instance class arity env)
- (-> Text ls;Arity (List Variable) $;Inst)
- (let [captureI (|> env
- (list/map (function [source]
- (if (variableL;captured? source)
- ($i;GETFIELD class (captured (variableL;captured-register source)) $Object)
- ($i;ALOAD (int-to-nat source)))))
- $i;fuse)
- argsI (if (poly-arg? arity)
- (|> (nullsI (n.dec arity))
- (list ($i;int 0))
- $i;fuse)
- id)]
- (|>. ($i;NEW class)
- $i;DUP
- captureI
- argsI
- ($i;INVOKESPECIAL class "<init>" (init-method env arity) false))))
+ (-> Text ls;Arity (List Variable) (Meta $;Inst))
+ (do meta;Monad<Meta>
+ [captureI+ (monad;map @ referenceT;translate-variable env)
+ #let [argsI (if (poly-arg? arity)
+ (|> (nullsI (n.dec arity))
+ (list ($i;int 0))
+ $i;fuse)
+ id)]]
+ (wrap (|>. ($i;NEW class)
+ $i;DUP
+ ($i;fuse captureI+)
+ argsI
+ ($i;INVOKESPECIAL class "<init>" (init-method env arity) false)))))
(def: (with-reset class arity env)
(-> Text ls;Arity (List Variable) $;Def)
@@ -138,7 +126,7 @@
_ (list;n.range +0 (n.dec env-size)))
(list/map (function [source]
(|>. ($i;ALOAD +0)
- ($i;GETFIELD class (captured source) $Object))))
+ ($i;GETFIELD class (referenceT;captured source) $Object))))
$i;fuse)
argsI (|> (nullsI (n.dec arity))
(list ($i;int 0))
@@ -182,7 +170,7 @@
(list/map (function [register]
(|>. ($i;ALOAD +0)
($i;ALOAD (n.inc register))
- ($i;PUTFIELD class (captured register) $Object))))
+ ($i;PUTFIELD class (referenceT;captured register) $Object))))
$i;fuse)
store-partialI (if (poly-arg? arity)
(|> (list;n.range +0 (n.- +2 arity))
@@ -190,7 +178,7 @@
(let [register (offset-partial idx)]
(|>. ($i;ALOAD +0)
($i;ALOAD (n.inc register))
- ($i;PUTFIELD class (partial idx) $Object)))))
+ ($i;PUTFIELD class (referenceT;partial idx) $Object)))))
$i;fuse)
id)]
($d;method #$;Public $;noneM "<init>" (init-method env arity)
@@ -212,7 +200,7 @@
(list/map (function [[stage @label]]
(let [load-partialsI (if (n.> +0 stage)
(|> (list;n.range +0 (n.dec stage))
- (list/map (|>. partial (load-fieldI class)))
+ (list/map (|>. referenceT;partial (load-fieldI class)))
$i;fuse)
id)]
(cond (i.= arity-over-extent (nat-to-int stage))
@@ -242,7 +230,7 @@
load-capturedI (|> (case env-size
+0 (list)
_ (list;n.range +0 (n.dec env-size)))
- (list/map (|>. captured (load-fieldI class)))
+ (list/map (|>. referenceT;captured (load-fieldI class)))
$i;fuse)]
(|>. ($i;label @label)
($i;NEW class)
@@ -269,7 +257,7 @@
(def: #export (with-function @begin class env arity bodyI)
(-> $;Label Text (List Variable) ls;Arity $;Inst
- [$;Def $;Inst])
+ (Meta [$;Def $;Inst]))
(let [env-size (list;size env)
applyD (: $;Def
(if (poly-arg? arity)
@@ -289,9 +277,10 @@
(with-init class env arity)
(with-reset class arity env)
applyD
- ))
- instanceI (instance class arity env)]
- [functionD instanceI]))
+ ))]
+ (do meta;Monad<Meta>
+ [instanceI (instance class arity env)]
+ (wrap [functionD instanceI]))))
(def: #export (translate-function translate env arity bodyS)
(-> (-> ls;Synthesis (Meta $;Inst))
@@ -302,7 +291,7 @@
[function-class bodyI] (hostL;with-sub-context
(hostL;with-anchor [@begin +1]
(translate bodyS)))
- #let [[functionD instanceI] (with-function @begin function-class env arity bodyI)]
+ [functionD instanceI] (with-function @begin function-class env arity bodyI)
_ (commonT;store-class function-class
($d;class #$;V1.6 #$;Public $;finalC
function-class (list)
diff --git a/new-luxc/source/luxc/lang/translation/reference.jvm.lux b/new-luxc/source/luxc/lang/translation/reference.jvm.lux
index 3e835f8e1..8e229af9c 100644
--- a/new-luxc/source/luxc/lang/translation/reference.jvm.lux
+++ b/new-luxc/source/luxc/lang/translation/reference.jvm.lux
@@ -11,8 +11,16 @@
["$i" inst]))
(lang ["ls" synthesis]
[";L" variable #+ Variable]
- (translation [";T" common]
- [";T" function]))))
+ (translation [";T" common]))))
+
+(do-template [<name> <prefix>]
+ [(def: #export (<name> idx)
+ (-> Nat Text)
+ (|> idx nat-to-int %i (format <prefix>)))]
+
+ [captured "c"]
+ [partial "p"]
+ )
(def: #export (translate-captured variable)
(-> Variable (Meta $;Inst))
@@ -20,13 +28,19 @@
[function-class hostL;context]
(wrap (|>. ($i;ALOAD +0)
($i;GETFIELD function-class
- (|> variable i.inc (i.* -1) int-to-nat functionT;captured)
+ (|> variable i.inc (i.* -1) int-to-nat captured)
commonT;$Object)))))
-(def: #export (translate-variable variable)
+(def: #export (translate-local variable)
(-> Variable (Meta $;Inst))
(meta/wrap ($i;ALOAD (int-to-nat variable))))
+(def: #export (translate-variable variable)
+ (-> Variable (Meta $;Inst))
+ (if (variableL;captured? variable)
+ (translate-captured variable)
+ (translate-local variable)))
+
(def: #export (translate-definition [def-module def-name])
(-> Ident (Meta $;Inst))
(let [bytecode-name (format def-module "/" (&;normalize-name def-name))]
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)