aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/lux/type/check.lux106
1 files changed, 48 insertions, 58 deletions
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index e1324a691..3a2b96635 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -43,9 +43,7 @@
(type: #export Var Nat)
-(type: #export Assumption
- {#subsumption [Type Type]
- #verdict Bit})
+(type: #export Assumption [Type Type])
(type: #export (Check a)
(-> Type-Context (Error [Type-Context a])))
@@ -343,16 +341,15 @@
(right context))))
(def: (assumed? [e a] assumptions)
- (-> [Type Type] (List Assumption) (Maybe Bit))
- (:: maybe.Monad<Maybe> map product.right
- (list.find (function (_ [[fe fa] status])
- (and (type/= e fe)
- (type/= a fa)))
- assumptions)))
+ (-> Assumption (List Assumption) Bit)
+ (list.any? (function (_ [e' a'])
+ (and (type/= e e')
+ (type/= a a')))
+ assumptions))
-(def: (assume! ea status assumptions)
- (-> [Type Type] Bit (List Assumption) (List Assumption))
- (#.Cons [ea status] assumptions))
+(def: (assume! assumption assumptions)
+ (-> Assumption (List Assumption) (List Assumption))
+ (#.Cons assumption assumptions))
(def: (if-bind id type then else)
(All [a]
@@ -384,7 +381,7 @@
(update (#.Var to) interpose)))
(def: (check-vars check' assumptions idE idA)
- (-> (-> Type Type (List Assumption) (Check (List Assumption)))
+ (-> (-> (List Assumption) Type Type (Check (List Assumption)))
(List Assumption)
Var Var
(Check (List Assumption)))
@@ -409,7 +406,7 @@
(wrap assumptions))
_
- (check' etype (#.Var idA) assumptions))
+ (check' assumptions etype (#.Var idA)))
## Interpose new variable between 2 existing links
[#.None (#.Some atype)]
@@ -420,7 +417,7 @@
(wrap assumptions))
_
- (check' (#.Var idE) atype assumptions))
+ (check' assumptions (#.Var idE) atype))
[(#.Some etype) (#.Some atype)]
(case [etype atype]
@@ -453,7 +450,7 @@
(wrap assumptions))
_
- (check' etype atype assumptions))))))
+ (check' assumptions etype atype))))))
(def: (with-error-stack on-error check)
(All [a] (-> (-> Any Text) (Check a) (Check a)))
@@ -476,59 +473,59 @@
output)))
(def: (check-apply check' assumptions [eAT eFT] [aAT aFT])
- (-> (-> Type Type (List Assumption) (Check (List Assumption))) (List Assumption)
+ (-> (-> (List Assumption) Type Type (Check (List Assumption))) (List Assumption)
[Type Type] [Type Type]
(Check (List Assumption)))
(case [eFT aFT]
(^or [(#.UnivQ _ _) (#.Ex _)] [(#.UnivQ _ _) (#.Var _)])
(do Monad<Check>
[eFT' (apply-type! eFT eAT)]
- (check' eFT' (#.Apply aAT aFT) assumptions))
+ (check' assumptions eFT' (#.Apply aAT aFT)))
(^or [(#.Ex _) (#.UnivQ _ _)] [(#.Var _) (#.UnivQ _ _)])
(do Monad<Check>
[aFT' (apply-type! aFT aAT)]
- (check' (#.Apply eAT eFT) aFT' assumptions))
+ (check' assumptions (#.Apply eAT eFT) aFT'))
(^or [(#.Ex _) _] [_ (#.Ex _)])
(do Monad<Check>
- [assumptions (check' eFT aFT assumptions)]
- (check' eAT aAT assumptions))
+ [assumptions (check' assumptions eFT aFT)]
+ (check' assumptions eAT aAT))
[(#.Var id) _]
(do Monad<Check>
[?rFT (read id)]
(case ?rFT
(#.Some rFT)
- (check' (#.Apply eAT rFT) (#.Apply aAT aFT) assumptions)
+ (check' assumptions (#.Apply eAT rFT) (#.Apply aAT aFT))
_
(do Monad<Check>
- [assumptions (check' eFT aFT assumptions)
+ [assumptions (check' assumptions eFT aFT)
e' (apply-type! aFT eAT)
a' (apply-type! aFT aAT)]
- (check' e' a' assumptions))))
+ (check' assumptions e' a'))))
[_ (#.Var id)]
(do Monad<Check>
[?rFT (read id)]
(case ?rFT
(#.Some rFT)
- (check' (#.Apply eAT eFT) (#.Apply aAT rFT) assumptions)
+ (check' assumptions (#.Apply eAT eFT) (#.Apply aAT rFT))
_
(do Monad<Check>
- [assumptions (check' eFT aFT assumptions)
+ [assumptions (check' assumptions eFT aFT)
e' (apply-type! eFT eAT)
a' (apply-type! eFT aAT)]
- (check' e' a' assumptions))))
+ (check' assumptions e' a'))))
_
(fail "")))
-(def: #export (check' expected actual assumptions)
+(def: #export (check' assumptions expected actual)
{#.doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
- (-> Type Type (List Assumption) (Check (List Assumption)))
+ (-> (List Assumption) Type Type (Check (List Assumption)))
(if (is? expected actual)
(check/wrap assumptions)
(with-error-stack
@@ -541,13 +538,13 @@
(if-bind id actual
(check/wrap assumptions)
(function (_ bound)
- (check' bound actual assumptions)))
+ (check' assumptions bound actual)))
[_ (#.Var id)]
(if-bind id expected
(check/wrap assumptions)
(function (_ bound)
- (check' expected bound assumptions)))
+ (check' assumptions expected bound)))
(^template [<fe> <fa>]
[(#.Apply A1 <fe>) (#.Apply A2 <fa>)]
@@ -559,28 +556,23 @@
[(#.Apply A F) _]
(let [fx-pair [expected actual]]
- (case (assumed? fx-pair assumptions)
- (#.Some ?)
- (if ?
- (check/wrap assumptions)
- (fail ""))
-
- #.None
+ (if (assumed? fx-pair assumptions)
+ (check/wrap assumptions)
(do Monad<Check>
[expected' (apply-type! F A)]
- (check' expected' actual (assume! fx-pair #1 assumptions)))))
+ (check' (assume! fx-pair assumptions) expected' actual))))
[_ (#.Apply A F)]
(do Monad<Check>
[actual' (apply-type! F A)]
- (check' expected actual' assumptions))
+ (check' assumptions expected actual'))
(^template [<tag> <instancer>]
[(<tag> _) _]
(do Monad<Check>
[[_ paramT] <instancer>
expected' (apply-type! expected paramT)]
- (check' expected' actual assumptions)))
+ (check' assumptions expected' actual)))
([#.UnivQ ..existential]
[#.ExQ ..var])
@@ -589,23 +581,23 @@
(do Monad<Check>
[[_ paramT] <instancer>
actual' (apply-type! actual paramT)]
- (check' expected actual' assumptions)))
+ (check' assumptions expected actual')))
([#.UnivQ ..var]
[#.ExQ ..existential])
[(#.Primitive e-name e-params) (#.Primitive a-name a-params)]
(if (!text/= e-name a-name)
- (loop [e-params e-params
- a-params a-params
- assumptions assumptions]
+ (loop [assumptions assumptions
+ e-params e-params
+ a-params a-params]
(case [e-params a-params]
[#.Nil #.Nil]
(check/wrap assumptions)
[(#.Cons e-head e-tail) (#.Cons a-head a-tail)]
(do Monad<Check>
- [assumptions' (check' e-head a-head assumptions)]
- (recur e-tail a-tail assumptions'))
+ [assumptions' (check' assumptions e-head a-head)]
+ (recur assumptions' e-tail a-tail))
_
(fail "")))
@@ -614,15 +606,15 @@
(^template [<compose>]
[(<compose> eL eR) (<compose> aL aR)]
(do Monad<Check>
- [assumptions (check' eL aL assumptions)]
- (check' eR aR assumptions)))
+ [assumptions (check' assumptions eL aL)]
+ (check' assumptions eR aR)))
([#.Sum]
[#.Product])
[(#.Function eI eO) (#.Function aI aO)]
(do Monad<Check>
- [assumptions (check' aI eI assumptions)]
- (check' eO aO assumptions))
+ [assumptions (check' assumptions aI eI)]
+ (check' assumptions eO aO))
[(#.Ex e!id) (#.Ex a!id)]
(if (!n/= e!id a!id)
@@ -630,10 +622,10 @@
(fail ""))
[(#.Named _ ?etype) _]
- (check' ?etype actual assumptions)
+ (check' assumptions ?etype actual)
[_ (#.Named _ ?atype)]
- (check' expected ?atype assumptions)
+ (check' assumptions expected ?atype)
_
(fail "")))))
@@ -641,15 +633,13 @@
(def: #export (check expected actual)
{#.doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
(-> Type Type (Check Any))
- (do Monad<Check>
- [assumptions (check' expected actual (list))]
- (wrap [])))
+ (check' (list) expected actual))
(def: #export (checks? expected actual)
{#.doc "A simple type-checking function that just returns a yes/no answer."}
(-> Type Type Bit)
- (case (run fresh-context (check expected actual))
- (#error.Error error)
+ (case (run fresh-context (check' (list) expected actual))
+ (#error.Error _)
#0
(#error.Success _)
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 17:29:32 +0000