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.lux130
1 files changed, 65 insertions, 65 deletions
diff --git a/stdlib/source/lux/type/check.lux b/stdlib/source/lux/type/check.lux
index 56198f5ab..e8f24102c 100644
--- a/stdlib/source/lux/type/check.lux
+++ b/stdlib/source/lux/type/check.lux
@@ -10,14 +10,14 @@
maybe
[product]
(coll [list])
- [error #- fail])
+ ["R" result])
[type "Type/" Eq<Type>]
))
(type: #export Fixed (List [[Type Type] Bool]))
(type: #export (Check a)
- (-> Type-Context (Error [Type-Context a])))
+ (-> Type-Context (R;Result [Type-Context a])))
(type: #export Type-Vars
(List [Nat (Maybe Type)]))
@@ -26,11 +26,11 @@
(def: (map f fa)
(function [context]
(case (fa context)
- (#;Left error)
- (#;Left error)
+ (#R;Error error)
+ (#R;Error error)
- (#;Right [context' output])
- (#;Right [context' (f output)])
+ (#R;Success [context' output])
+ (#R;Success [context' (f output)])
))))
(struct: #export _ (Applicative Check)
@@ -38,21 +38,21 @@
(def: (wrap x)
(function [context]
- (#;Right [context x])))
+ (#R;Success [context x])))
(def: (apply ff fa)
(function [context]
(case (ff context)
- (#;Right [context' f])
+ (#R;Success [context' f])
(case (fa context')
- (#;Right [context'' a])
- (#;Right [context'' (f a)])
+ (#R;Success [context'' a])
+ (#R;Success [context'' (f a)])
- (#;Left error)
- (#;Left error))
+ (#R;Error error)
+ (#R;Error error))
- (#;Left error)
- (#;Left error)
+ (#R;Error error)
+ (#R;Error error)
)))
)
@@ -62,16 +62,16 @@
(def: (join ffa)
(function [context]
(case (ffa context)
- (#;Right [context' fa])
+ (#R;Success [context' fa])
(case (fa context')
- (#;Right [context'' a])
- (#;Right [context'' a])
+ (#R;Success [context'' a])
+ (#R;Success [context'' a])
- (#;Left error)
- (#;Left error))
+ (#R;Error error)
+ (#R;Error error))
- (#;Left error)
- (#;Left error)
+ (#R;Error error)
+ (#R;Error error)
)))
)
@@ -121,93 +121,93 @@
## [[Logic]]
(def: #export (run context proc)
- (All [a] (-> Type-Context (Check a) (Error a)))
+ (All [a] (-> Type-Context (Check a) (R;Result a)))
(case (proc context)
- (#;Left error)
- (#;Left error)
+ (#R;Error error)
+ (#R;Error error)
- (#;Right [context' output])
- (#;Right output)))
+ (#R;Success [context' output])
+ (#R;Success output)))
(def: (apply-type! t-func t-arg)
(-> Type Type (Check Type))
(function [context]
(case (type;apply-type t-func t-arg)
#;None
- (#;Left (format "Invalid type application: " (%type t-func) " on " (%type t-arg)))
+ (#R;Error (format "Invalid type application: " (%type t-func) " on " (%type t-arg)))
(#;Some output)
- (#;Right [context output]))))
+ (#R;Success [context output]))))
(def: #export existential
{#;doc "A producer of existential types."}
(Check [Nat Type])
(function [context]
(let [id (get@ #;ex-counter context)]
- (#;Right [(update@ #;ex-counter n.inc context)
- [id (#;Ex id)]]))))
+ (#R;Success [(update@ #;ex-counter n.inc context)
+ [id (#;Ex id)]]))))
(def: #export (bound? id)
(-> Nat (Check Bool))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some _))
- (#;Right [context true])
+ (#R;Success [context true])
(#;Some #;None)
- (#;Right [context false])
+ (#R;Success [context false])
#;None
- (#;Left (format "Unknown type-var: " (%n id))))))
+ (#R;Error (format "Unknown type-var: " (%n id))))))
(def: #export (read-var id)
(-> Nat (Check Type))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some type))
- (#;Right [context type])
+ (#R;Success [context type])
(#;Some #;None)
- (#;Left (format "Unbound type-var: " (%n id)))
+ (#R;Error (format "Unbound type-var: " (%n id)))
#;None
- (#;Left (format "Unknown type-var: " (%n id))))))
+ (#R;Error (format "Unknown type-var: " (%n id))))))
(def: #export (write-var id type)
(-> Nat Type (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some (#;Some bound))
- (#;Left (format "Cannot rebind type-var: " (%n id) " | Current type: " (%type bound)))
+ (#R;Error (format "Cannot rebind type-var: " (%n id) " | Current type: " (%type bound)))
(#;Some #;None)
- (#;Right [(update@ #;var-bindings (var::put id (#;Some type)) context)
- []])
+ (#R;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
+ []])
#;None
- (#;Left (format "Unknown type-var: " (%n id))))))
+ (#R;Error (format "Unknown type-var: " (%n id))))))
(def: (rewrite-var id type)
(-> Nat Type (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#;Right [(update@ #;var-bindings (var::put id (#;Some type)) context)
- []])
+ (#R;Success [(update@ #;var-bindings (var::put id (#;Some type)) context)
+ []])
#;None
- (#;Left (format "Unknown type-var: " (%n id))))))
+ (#R;Error (format "Unknown type-var: " (%n id))))))
(def: #export (clear-var id)
(-> Nat (Check Unit))
(function [context]
(case (|> context (get@ #;var-bindings) (var::get id))
(#;Some _)
- (#;Right [(update@ #;var-bindings (var::put id #;None) context)
- []])
+ (#R;Success [(update@ #;var-bindings (var::put id #;None) context)
+ []])
#;None
- (#;Left (format "Unknown type-var: " (%n id))))))
+ (#R;Error (format "Unknown type-var: " (%n id))))))
(def: #export (clean t-id type)
(-> Nat Type (Check Type))
@@ -274,22 +274,22 @@
(Check [Nat Type])
(function [context]
(let [id (get@ #;var-counter context)]
- (#;Right [(|> context
- (update@ #;var-counter n.inc)
- (update@ #;var-bindings (var::put id #;None)))
- [id (#;Var id)]]))))
+ (#R;Success [(|> context
+ (update@ #;var-counter n.inc)
+ (update@ #;var-bindings (var::put id #;None)))
+ [id (#;Var id)]]))))
(def: get-bindings
(Check (List [Nat (Maybe Type)]))
(function [context]
- (#;Right [context
- (get@ #;var-bindings context)])))
+ (#R;Success [context
+ (get@ #;var-bindings context)])))
(def: (set-bindings value)
(-> (List [Nat (Maybe Type)]) (Check Unit))
(function [context]
- (#;Right [(set@ #;var-bindings value context)
- []])))
+ (#R;Success [(set@ #;var-bindings value context)
+ []])))
(def: #export (delete-var id)
(-> Nat (Check Unit))
@@ -343,16 +343,16 @@
(All [a] (-> (Check a) (Check (Maybe a))))
(function [context]
(case (op context)
- (#;Right [context' output])
- (#;Right [context' (#;Some output)])
+ (#R;Success [context' output])
+ (#R;Success [context' (#;Some output)])
- (#;Left _)
- (#;Right [context #;None]))))
+ (#R;Error _)
+ (#R;Success [context #;None]))))
(def: #export (fail message)
(All [a] (-> Text (Check a)))
(function [context]
- (#;Left message)))
+ (#R;Error message)))
(def: (fail-check expected actual)
(All [a] (-> Type Type (Check a)))
@@ -363,10 +363,10 @@
(All [a] (-> (Check a) (Check a) (Check a)))
(function [context]
(case (left context)
- (#;Right [context' output])
- (#;Right [context' output])
+ (#R;Success [context' output])
+ (#R;Success [context' output])
- (#;Left _)
+ (#R;Error _)
(right context))))
(def: (fx-get [e a] fixed)
@@ -555,13 +555,13 @@
{#;doc "A simple type-checking function that just returns a yes/no answer."}
(-> Type Type Bool)
(case (run fresh-context (check expected actual))
- (#;Left error)
+ (#R;Error error)
false
- (#;Right _)
+ (#R;Success _)
true))
(def: #export get-context
(Check Type-Context)
(function [context]
- (#;Right [context context])))
+ (#R;Success [context context])))
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-13 01:24:33 +0000