aboutsummaryrefslogtreecommitdiff
path: root/stdlib/source/lux/type/check.lux
diff options
context:
space:
mode:
Diffstat (limited to 'stdlib/source/lux/type/check.lux')
-rw-r--r--stdlib/source/lux/type/check.lux164
1 files changed, 82 insertions, 82 deletions
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 769b45391..f51ba5a15 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -2,57 +2,57 @@
Very useful for writing advanced macros."}
lux
- (lux (control ["F" functor]
- ["A" applicative]
- ["M" monad #+ do Monad])
+ (lux (control [functor #+ Functor]
+ [applicative #+ Applicative]
+ [monad #+ do Monad])
(data [text "text/" Monoid<Text> Eq<Text>]
[number "nat/" Codec<Text,Nat>]
maybe
[product]
(coll [list])
- ["R" result])
- [type "Type/" Eq<Type>]
+ ["E" error])
+ [type "type/" Eq<Type>]
))
(type: #export Assumptions (List [[Type Type] Bool]))
(type: #export (Check a)
- (-> Type-Context (R;Result [Type-Context a])))
+ (-> Type-Context (E;Error [Type-Context a])))
(type: #export Type-Vars
(List [Nat (Maybe Type)]))
-(struct: #export _ (F;Functor Check)
+(struct: #export _ (Functor Check)
(def: (map f fa)
(function [context]
(case (fa context)
- (#R;Error error)
- (#R;Error error)
+ (#E;Error error)
+ (#E;Error error)
- (#R;Success [context' output])
- (#R;Success [context' (f output)])
+ (#E;Success [context' output])
+ (#E;Success [context' (f output)])
))))
-(struct: #export _ (A;Applicative Check)
+(struct: #export _ (Applicative Check)
(def: functor Functor<Check>)
(def: (wrap x)
(function [context]
- (#R;Success [context x])))
+ (#E;Success [context x])))
(def: (apply ff fa)
(function [context]
(case (ff context)
- (#R;Success [context' f])
+ (#E;Success [context' f])
(case (fa context')
- (#R;Success [context'' a])
- (#R;Success [context'' (f a)])
+ (#E;Success [context'' a])
+ (#E;Success [context'' (f a)])
- (#R;Error error)
- (#R;Error error))
+ (#E;Error error)
+ (#E;Error error))
- (#R;Error error)
- (#R;Error error)
+ (#E;Error error)
+ (#E;Error error)
)))
)
@@ -62,20 +62,20 @@
(def: (join ffa)
(function [context]
(case (ffa context)
- (#R;Success [context' fa])
+ (#E;Success [context' fa])
(case (fa context')
- (#R;Success [context'' a])
- (#R;Success [context'' a])
+ (#E;Success [context'' a])
+ (#E;Success [context'' a])
- (#R;Error error)
- (#R;Error error))
+ (#E;Error error)
+ (#E;Error error))
- (#R;Error error)
- (#R;Error error)
+ (#E;Error error)
+ (#E;Error error)
)))
)
-(open Monad<Check> "Check/")
+(open Monad<Check> "check/")
(def: (var::get id plist)
(-> Nat Type-Vars (Maybe (Maybe Type)))
@@ -121,30 +121,30 @@
## [[Logic]]
(def: #export (run context proc)
- (All [a] (-> Type-Context (Check a) (R;Result a)))
+ (All [a] (-> Type-Context (Check a) (E;Error a)))
(case (proc context)
- (#R;Error error)
- (#R;Error error)
+ (#E;Error error)
+ (#E;Error error)
- (#R;Success [context' output])
- (#R;Success output)))
+ (#E;Success [context' output])
+ (#E;Success output)))
(def: (apply-type! t-func t-arg)
(-> Type Type (Check Type))
(function [context]
(case (type;apply (list t-arg) t-func)
#;None
- (#R;Error ($_ text/compose "Invalid type application: " (type;to-text t-func) " on " (type;to-text t-arg)))
+ (#E;Error ($_ text/compose "Invalid type application: " (type;to-text t-func) " on " (type;to-text t-arg)))
(#;Some output)
- (#R;Success [context output]))))
+ (#E;Success [context output]))))
(def: #export existential
{#;doc "A producer of existential types."}
(Check [Nat Type])
(function [context]
(let [id (get@ #;ex-counter context)]
- (#R;Success [(update@ #;ex-counter n.inc context)
+ (#E;Success [(update@ #;ex-counter n.inc context)
[id (#;Ex id)]]))))
(def: #export (bound? id)
@@ -152,62 +152,62 @@
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some _))
- (#R;Success [context true])
+ (#E;Success [context true])
(#;Some #;None)
- (#R;Success [context false])
+ (#E;Success [context false])
#;None
- (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
(def: #export (read id)
(-> Nat (Check Type))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some type))
- (#R;Success [context type])
+ (#E;Success [context type])
(#;Some #;None)
- (#R;Error ($_ text/compose "Unbound type-var: " (nat/encode id)))
+ (#E;Error ($_ text/compose "Unbound type-var: " (nat/encode id)))
#;None
- (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
(def: #export (write id type)
(-> Nat Type (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some bound))
- (#R;Error ($_ text/compose "Cannot rebind type-var: " (nat/encode id) " | Current type: " (type;to-text bound)))
+ (#E;Error ($_ text/compose "Cannot rebind type-var: " (nat/encode id) " | Current type: " (type;to-text bound)))
(#;Some #;None)
- (#R;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
+ (#E;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
[]])
#;None
- (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
(def: (update id type)
(-> Nat Type (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#R;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
+ (#E;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
[]])
#;None
- (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
(def: #export (clear id)
(-> Nat (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#R;Success [(update@ #;var-bindings (var::put id #;None) context)
+ (#E;Success [(update@ #;var-bindings (var::put id #;None) context)
[]])
#;None
- (#R;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
+ (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id))))))
(def: #export (clean t-id type)
(-> Nat Type (Check Type))
@@ -243,7 +243,7 @@
(#;Host name params)
(do Monad<Check>
- [=params (M;map @ (clean t-id) params)]
+ [=params (monad;map @ (clean t-id) params)]
(wrap (#;Host name =params)))
(^template [<tag>]
@@ -260,7 +260,7 @@
(^template [<tag>]
(<tag> env body)
(do Monad<Check>
- [=env (M;map @ (clean t-id) env)
+ [=env (monad;map @ (clean t-id) env)
=body (clean t-id body)] ## TODO: DO NOT CLEAN THE BODY
(wrap (<tag> =env =body))))
([#;UnivQ]
@@ -274,7 +274,7 @@
(Check [Nat Type])
(function [context]
(let [id (get@ #;var-counter context)]
- (#R;Success [(|> context
+ (#E;Success [(|> context
(update@ #;var-counter n.inc)
(update@ #;var-bindings (var::put id #;None)))
[id (#;Var id)]]))))
@@ -282,19 +282,19 @@
(def: get-bindings
(Check (List [Nat (Maybe Type)]))
(function [context]
- (#R;Success [context
+ (#E;Success [context
(get@ #;var-bindings context)])))
(def: (set-bindings value)
(-> (List [Nat (Maybe Type)]) (Check Unit))
(function [context]
- (#R;Success [(set@ #;var-bindings value context)
+ (#E;Success [(set@ #;var-bindings value context)
[]])))
(def: #export (delete id)
(-> Nat (Check Unit))
(function [context]
- (#R;Success [(update@ #;var-bindings (var::remove id) context)
+ (#E;Success [(update@ #;var-bindings (var::remove id) context)
[]])))
(def: #export (with k)
@@ -316,16 +316,16 @@
(All [a] (-> (Check a) (Check (Maybe a))))
(function [context]
(case (op context)
- (#R;Success [context' output])
- (#R;Success [context' (#;Some output)])
+ (#E;Success [context' output])
+ (#E;Success [context' (#;Some output)])
- (#R;Error _)
- (#R;Success [context #;None]))))
+ (#E;Error _)
+ (#E;Success [context #;None]))))
(def: #export (fail message)
(All [a] (-> Text (Check a)))
(function [context]
- (#R;Error message)))
+ (#E;Error message)))
(def: (fail-check expected actual)
(All [a] (-> Type Type (Check a)))
@@ -337,18 +337,18 @@
(All [a] (-> (Check a) (Check a) (Check a)))
(function [context]
(case (left context)
- (#R;Success [context' output])
- (#R;Success [context' output])
+ (#E;Success [context' output])
+ (#E;Success [context' output])
- (#R;Error _)
+ (#E;Error _)
(right context))))
(def: (assumed? [e a] assumptions)
(-> [Type Type] Assumptions (Maybe Bool))
(:: Monad<Maybe> map product;right
(list;find (function [[[fe fa] status]]
- (and (Type/= e fe)
- (Type/= a fa)))
+ (and (type/= e fe)
+ (type/= a fa)))
assumptions)))
(def: (assume! ea status assumptions)
@@ -370,11 +370,11 @@
{#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."}
(-> Type Type Assumptions (Check Assumptions))
(if (is expected actual)
- (Check/wrap assumptions)
+ (check/wrap assumptions)
(case [expected actual]
[(#;Var e-id) (#;Var a-id)]
(if (n.= e-id a-id)
- (Check/wrap assumptions)
+ (check/wrap assumptions)
(do Monad<Check>
[ebound (attempt (read e-id))
abound (attempt (read a-id))]
@@ -394,12 +394,12 @@
(check' etype atype assumptions))))
[(#;Var id) _]
- (on id actual (Check/wrap assumptions)
+ (on id actual (check/wrap assumptions)
(function [bound]
(check' bound actual assumptions)))
[_ (#;Var id)]
- (on id expected (Check/wrap assumptions)
+ (on id expected (check/wrap assumptions)
(function [bound]
(check' expected bound assumptions)))
@@ -433,7 +433,7 @@
(case (assumed? fx-pair assumptions)
(#;Some ?)
(if ?
- (Check/wrap assumptions)
+ (check/wrap assumptions)
(fail-check expected actual))
#;None
@@ -459,7 +459,7 @@
[actual' (apply-type! actual var)
assumptions (check' expected actual' assumptions)
_ (clean var-id expected)]
- (Check/wrap assumptions))))
+ (check/wrap assumptions))))
[(#;ExQ e!env e!def) _]
(with
@@ -468,7 +468,7 @@
[expected' (apply-type! expected var)
assumptions (check' expected' actual assumptions)
_ (clean var-id actual)]
- (Check/wrap assumptions))))
+ (check/wrap assumptions))))
[_ (#;ExQ a!env a!def)]
(do Monad<Check>
@@ -481,16 +481,16 @@
(n.= (list;size e-params)
(list;size a-params)))
(do Monad<Check>
- [assumptions (M;fold Monad<Check>
- (function [[e a] assumptions] (check' e a assumptions))
- assumptions
- (list;zip2 e-params a-params))]
- (Check/wrap assumptions))
+ [assumptions (monad;fold Monad<Check>
+ (function [[e a] assumptions] (check' e a assumptions))
+ assumptions
+ (list;zip2 e-params a-params))]
+ (check/wrap assumptions))
(fail-check expected actual))
(^template [<identity> <compose>]
[<identity> <identity>]
- (Check/wrap assumptions)
+ (check/wrap assumptions)
[(<compose> eL eR) (<compose> aL aR)]
(do Monad<Check>
@@ -506,7 +506,7 @@
[(#;Ex e!id) (#;Ex a!id)]
(if (n.= e!id a!id)
- (Check/wrap assumptions)
+ (check/wrap assumptions)
(fail-check expected actual))
[(#;Named _ ?etype) _]
@@ -529,13 +529,13 @@
{#;doc "A simple type-checking function that just returns a yes/no answer."}
(-> Type Type Bool)
(case (run fresh-context (check expected actual))
- (#R;Error error)
+ (#E;Error error)
false
- (#R;Success _)
+ (#E;Success _)
true))
(def: #export get-context
(Check Type-Context)
(function [context]
- (#R;Success [context context])))
+ (#E;Success [context context])))
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-13 01:39:14 +0000