aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/library/lux/type/check.lux
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--stdlib/source/library/lux/type/check.lux65
1 files changed, 33 insertions, 32 deletions
diff --git a/stdlib/source/library/lux/type/check.lux b/stdlib/source/library/lux/type/check.lux
index f01edbe64..fc3b31347 100644
--- a/stdlib/source/library/lux/type/check.lux
+++ b/stdlib/source/library/lux/type/check.lux
@@ -1,4 +1,5 @@
-(.module: {#.doc "Type-checking functionality."}
+(.module:
+ {#.doc "Type-checking functionality."}
[library
[lux #*
["@" target]
@@ -104,7 +105,7 @@
(def: &functor ..functor)
- (def: (wrap x)
+ (def: (in x)
(function (_ context)
(#try.Success [context x])))
@@ -177,7 +178,7 @@
(#try.Success [context []])
(#try.Failure message))))
-(def: #export (throw exception message)
+(def: #export (except exception message)
(All [e a] (-> (Exception e) e (Check a)))
(..failure (exception.construct exception message)))
@@ -202,7 +203,7 @@
(#try.Success [context <succeed>])
#.None
- (exception.throw ..unknown_type_var id))))]
+ (exception.except ..unknown_type_var id))))]
[bound? Bit false true]
[read (Maybe Type) #.None (#.Some bound)]
@@ -214,10 +215,10 @@
[?type (read id)]
(case ?type
(#.Some type)
- (wrap type)
+ (in type)
#.None
- (..throw ..unbound_type_var id))))
+ (..except ..unbound_type_var id))))
(def: (peek id)
(-> Var (Check Type))
@@ -227,10 +228,10 @@
(#try.Success [context bound])
(#.Some _)
- (exception.throw ..unbound_type_var id)
+ (exception.except ..unbound_type_var id)
_
- (exception.throw ..unknown_type_var id))))
+ (exception.except ..unknown_type_var id))))
(def: #export (bind type id)
(-> Type Var (Check Any))
@@ -241,10 +242,10 @@
[]])
(#.Some (#.Some bound))
- (exception.throw ..cannot_rebind_var [id type bound])
+ (exception.except ..cannot_rebind_var [id type bound])
_
- (exception.throw ..unknown_type_var id))))
+ (exception.except ..unknown_type_var id))))
(def: (update type id)
(-> Type Var (Check Any))
@@ -255,7 +256,7 @@
[]])
_
- (exception.throw ..unknown_type_var id))))
+ (exception.except ..unknown_type_var id))))
(def: #export var
(Check [Var Type])
@@ -277,7 +278,7 @@
(apply_type! funcT' argT)
_
- (throw ..invalid_type_application [funcT argT])))
+ (except ..invalid_type_application [funcT argT])))
(#.Apply argT' funcT')
(do ..monad
@@ -287,10 +288,10 @@
_
(case (//.applied (list argT) funcT)
(#.Some output)
- (check\wrap output)
+ (check\in output)
_
- (throw ..invalid_type_application [funcT argT]))))
+ (except ..invalid_type_application [funcT argT]))))
(type: Ring
(Set Var))
@@ -320,7 +321,7 @@
(#try.Success [context output])
#.None
- (exception.throw ..unknown_type_var current)))))
+ (exception.except ..unknown_type_var current)))))
(def: #export fresh_context
Type_Context
@@ -395,7 +396,7 @@
(def: (check_vars check' assumptions idE idA)
(-> (Checker Type) (Checker Var))
(if (!n\= idE idA)
- (check\wrap assumptions)
+ (check\in assumptions)
(do {! ..monad}
[ebound (attempt (peek idE))
abound (attempt (peek idA))]
@@ -404,7 +405,7 @@
[#.None #.None]
(do !
[_ (link_2 idE idA)]
- (wrap assumptions))
+ (in assumptions))
## Interpose new variable between 2 existing links
[(#.Some etype) #.None]
@@ -412,7 +413,7 @@
(#.Var targetE)
(do !
[_ (link_3 idA targetE idE)]
- (wrap assumptions))
+ (in assumptions))
_
(check' assumptions etype (#.Var idA)))
@@ -423,7 +424,7 @@
(#.Var targetA)
(do !
[_ (link_3 idE targetA idA)]
- (wrap assumptions))
+ (in assumptions))
_
(check' assumptions (#.Var idE) atype))
@@ -435,23 +436,23 @@
[ringE (..ring idE)
ringA (..ring idA)]
(if (\ set.equivalence = ringE ringA)
- (wrap assumptions)
+ (in assumptions)
## Fuse 2 rings
(do !
[_ (monad.fold ! (function (_ interpose to)
(do !
[_ (link_3 interpose to idE)]
- (wrap interpose)))
+ (in interpose)))
targetE
(set.to_list ringA))]
- (wrap assumptions))))
+ (in assumptions))))
(^template [<pattern> <id> <type>]
[<pattern>
(do !
[ring (..ring <id>)
_ (monad.map ! (update <type>) (set.to_list ring))]
- (wrap assumptions))])
+ (in assumptions))])
([[(#.Var _) _] idE atype]
[[_ (#.Var _)] idA etype])
@@ -559,7 +560,7 @@
(Checker Type)
(if (for {@.php false} ## TODO: Remove this once JPHP is gone.
(is? expected actual))
- (check\wrap assumptions)
+ (check\in assumptions)
(with ..type_check_failed [expected actual]
(case [expected actual]
[(#.Var idE) (#.Var idA)]
@@ -567,13 +568,13 @@
[(#.Var id) _]
(if_bind id actual
- (check\wrap assumptions)
+ (check\in assumptions)
(function (_ bound)
(check' assumptions bound actual)))
[_ (#.Var id)]
(if_bind id expected
- (check\wrap assumptions)
+ (check\in assumptions)
(function (_ bound)
(check' assumptions expected bound)))
@@ -588,7 +589,7 @@
[(#.Apply A F) _]
(let [new_assumption [expected actual]]
(if (assumed? new_assumption assumptions)
- (check\wrap assumptions)
+ (check\in assumptions)
(do ..monad
[expected' (apply_type! F A)]
(check' (assume! new_assumption assumptions) expected' actual))))
@@ -625,7 +626,7 @@
a_params a_params]
(case [e_params a_params]
[#.Nil #.Nil]
- (check\wrap assumptions)
+ (check\in assumptions)
[(#.Cons e_head e_tail) (#.Cons a_head a_tail)]
(do ..monad
@@ -651,7 +652,7 @@
[(#.Ex e!id) (#.Ex a!id)]
(if (!n\= e!id a!id)
- (check\wrap assumptions)
+ (check\in assumptions)
..silent_failure!)
[(#.Named _ ?etype) _]
@@ -692,7 +693,7 @@
(check\map (|>> (#.Primitive name))))
(^or (#.Parameter _) (#.Ex _) (#.Named _))
- (check\wrap inputT)
+ (check\in inputT)
(^template [<tag>]
[(<tag> leftT rightT)
@@ -710,12 +711,12 @@
(clean actualT)
_
- (wrap inputT)))
+ (in inputT)))
(^template [<tag>]
[(<tag> envT+ unquantifiedT)
(do {! ..monad}
[envT+' (monad.map ! clean envT+)]
- (wrap (<tag> envT+' unquantifiedT)))])
+ (in (<tag> envT+' unquantifiedT)))])
([#.UnivQ] [#.ExQ])
))