diff options
| -rw-r--r-- | stdlib/source/lux/meta/type/check.lux | 372 | ||||
| -rw-r--r-- | stdlib/test/test/lux/meta/type/check.lux | 115 |
2 files changed, 369 insertions, 118 deletions
diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux index 296aee11a..920eb876c 100644 --- a/stdlib/source/lux/meta/type/check.lux +++ b/stdlib/source/lux/meta/type/check.lux @@ -1,36 +1,38 @@ -(;module: {#;doc "Type-checking functionality. - - Very useful for writing advanced macros."} +(;module: {#;doc "Type-checking functionality."} lux (lux (control [functor #+ Functor] [applicative #+ Applicative] - [monad #+ do Monad]) + [monad #+ do Monad] + ["ex" exception #+ exception:]) (data [text "text/" Monoid<Text> Eq<Text>] [number "nat/" Codec<Text,Nat>] maybe [product] - (coll [list]) - ["E" error]) + (coll [list] + [set #+ Set]) + ["e" error]) (meta [type "type/" Eq<Type>]) )) +(type: #export Var Nat) + (type: #export Assumptions (List [[Type Type] Bool])) (type: #export (Check a) - (-> Type-Context (E;Error [Type-Context a]))) + (-> Type-Context (e;Error [Type-Context a]))) (type: #export Type-Vars - (List [Nat (Maybe Type)])) + (List [Var (Maybe Type)])) (struct: #export _ (Functor Check) (def: (map f fa) (function [context] (case (fa context) - (#E;Error error) - (#E;Error error) + (#e;Error error) + (#e;Error error) - (#E;Success [context' output]) - (#E;Success [context' (f output)]) + (#e;Success [context' output]) + (#e;Success [context' (f output)]) )))) (struct: #export _ (Applicative Check) @@ -38,21 +40,21 @@ (def: (wrap x) (function [context] - (#E;Success [context x]))) + (#e;Success [context x]))) (def: (apply ff fa) (function [context] (case (ff context) - (#E;Success [context' f]) + (#e;Success [context' f]) (case (fa context') - (#E;Success [context'' a]) - (#E;Success [context'' (f a)]) + (#e;Success [context'' a]) + (#e;Success [context'' (f a)]) - (#E;Error error) - (#E;Error error)) + (#e;Error error) + (#e;Error error)) - (#E;Error error) - (#E;Error error) + (#e;Error error) + (#e;Error error) ))) ) @@ -62,23 +64,23 @@ (def: (join ffa) (function [context] (case (ffa context) - (#E;Success [context' fa]) + (#e;Success [context' fa]) (case (fa context') - (#E;Success [context'' a]) - (#E;Success [context'' a]) + (#e;Success [context'' a]) + (#e;Success [context'' a]) - (#E;Error error) - (#E;Error error)) + (#e;Error error) + (#e;Error error)) - (#E;Error error) - (#E;Error error) + (#e;Error error) + (#e;Error error) ))) ) (open Monad<Check> "check/") (def: (var::get id plist) - (-> Nat Type-Vars (Maybe (Maybe Type))) + (-> Var Type-Vars (Maybe (Maybe Type))) (case plist #;Nil #;None @@ -91,7 +93,7 @@ )) (def: (var::put id value plist) - (-> Nat (Maybe Type) Type-Vars Type-Vars) + (-> Var (Maybe Type) Type-Vars Type-Vars) (case plist #;Nil (list [id value]) @@ -106,7 +108,7 @@ )) (def: (var::remove id plist) - (-> Nat Type-Vars Type-Vars) + (-> Var Type-Vars Type-Vars) (case plist #;Nil #;Nil @@ -121,96 +123,100 @@ ## [[Logic]] (def: #export (run context proc) - (All [a] (-> Type-Context (Check a) (E;Error a))) + (All [a] (-> Type-Context (Check a) (e;Error a))) (case (proc context) - (#E;Error error) - (#E;Error error) + (#e;Error error) + (#e;Error error) - (#E;Success [context' output]) - (#E;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 - (#E;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) - (#E;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)] - (#E;Success [(update@ #;ex-counter n.inc context) + (#e;Success [(update@ #;ex-counter n.inc context) [id (#;Ex id)]])))) +(exception: #export Unknown-Type-Var) +(exception: #export Unbound-Type-Var) +(exception: #export Improper-Ring) + (def: #export (bound? id) - (-> Nat (Check Bool)) + (-> Var (Check Bool)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) (#;Some (#;Some _)) - (#E;Success [context true]) + (#e;Success [context true]) (#;Some #;None) - (#E;Success [context false]) + (#e;Success [context false]) #;None - (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) + (ex;throw Unknown-Type-Var (nat/encode id))))) (def: #export (read id) - (-> Nat (Check Type)) + (-> Var (Check Type)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) (#;Some (#;Some type)) - (#E;Success [context type]) + (#e;Success [context type]) (#;Some #;None) - (#E;Error ($_ text/compose "Unbound type-var: " (nat/encode id))) + (ex;throw Unbound-Type-Var (nat/encode id)) #;None - (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) + (ex;throw Unknown-Type-Var (nat/encode id))))) -(def: #export (write id type) - (-> Nat Type (Check Unit)) +(def: #export (write type id) + (-> Type Var (Check Unit)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) (#;Some (#;Some bound)) - (#E;Error ($_ text/compose "Cannot rebind type-var: " (nat/encode id) " | Current type: " (type;to-text bound))) + (#e;Error ($_ text/compose "Cannot re-bind type-var: " (nat/encode id) " | Current type: " (type;to-text bound))) (#;Some #;None) - (#E;Success [(update@ #;var-bindings (var::put id (#;Some type)) context) + (#e;Success [(update@ #;var-bindings (var::put id (#;Some type)) context) []]) #;None - (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) + (ex;throw Unknown-Type-Var (nat/encode id))))) -(def: (update id type) - (-> Nat Type (Check Unit)) +(def: (update type id) + (-> Type Var (Check Unit)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) (#;Some _) - (#E;Success [(update@ #;var-bindings (var::put id (#;Some type)) context) + (#e;Success [(update@ #;var-bindings (var::put id (#;Some type)) context) []]) #;None - (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) + (ex;throw Unknown-Type-Var (nat/encode id))))) (def: #export (clear id) - (-> Nat (Check Unit)) + (-> Var (Check Unit)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) (#;Some _) - (#E;Success [(update@ #;var-bindings (var::put id #;None) context) + (#e;Success [(update@ #;var-bindings (var::put id #;None) context) []]) #;None - (#E;Error ($_ text/compose "Unknown type-var: " (nat/encode id)))))) + (ex;throw Unknown-Type-Var (nat/encode id))))) (def: #export (clean t-id type) - (-> Nat Type (Check Type)) + (-> Var Type (Check Type)) (case type (#;Var id) (if (n.= t-id id) @@ -232,12 +238,12 @@ [_ (clear id)] (wrap type)) (do Monad<Check> - [_ (update id ==type)] + [_ (update ==type id)] (wrap type))) _ (do Monad<Check> - [_ (update id ==type)] + [_ (update ==type id)] (wrap type)))) (wrap type)))) @@ -271,34 +277,97 @@ )) (def: #export create - (Check [Nat Type]) + (Check [Var Type]) (function [context] (let [id (get@ #;var-counter context)] - (#E;Success [(|> context + (#e;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)])) + (Check (List [Var (Maybe Type)])) (function [context] - (#E;Success [context + (#e;Success [context (get@ #;var-bindings context)]))) (def: (set-bindings value) - (-> (List [Nat (Maybe Type)]) (Check Unit)) + (-> (List [Var (Maybe Type)]) (Check Unit)) (function [context] - (#E;Success [(set@ #;var-bindings value context) + (#e;Success [(set@ #;var-bindings value context) []]))) -(def: #export (delete id) - (-> Nat (Check Unit)) +(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>)) + +(def: #export (ring id) + (-> Var (Check Ring)) + (function [context] + (loop [current id + output (set;add id empty-ring)] + (case (|> context (get@ #;var-bindings) (var::get current)) + (#;Some (#;Some type)) + (case type + (#;Var post) + (if (n.= id post) + (#e;Success [context output]) + (recur post (set;add post output))) + + _ + (#e;Success [context empty-ring])) + + (#;Some #;None) + (#e;Success [context output]) + + #;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) + (#e;Success [(update@ #;var-bindings (var::remove id) context) []]))) +(def: #export (delete id) + (-> Var (Check Unit)) + (do Monad<Check> + [?link (pre-link id)] + (case ?link + #;None + (delete' id) + + (#;Some pre) + (do @ + [post (read id) + _ (update post pre)] + (delete' id))))) + (def: #export (with k) - (All [a] (-> (-> [Nat Type] (Check a)) (Check a))) + (All [a] (-> (-> [Var Type] (Check a)) (Check a))) (do Monad<Check> [[id var] create output (k [id var]) @@ -316,16 +385,23 @@ (All [a] (-> (Check a) (Check (Maybe a)))) (function [context] (case (op context) - (#E;Success [context' output]) - (#E;Success [context' (#;Some output)]) + (#e;Success [context' output]) + (#e;Success [context' (#;Some output)]) - (#E;Error _) - (#E;Success [context #;None])))) + (#e;Error _) + (#e;Success [context #;None])))) (def: #export (fail message) (All [a] (-> Text (Check a))) (function [context] - (#E;Error message))) + (#e;Error message))) + +(def: #export (assert message test) + (-> Text Bool (Check Unit)) + (function [context] + (if test + (#e;Success [context []]) + (#e;Error message)))) (def: (fail-check expected actual) (All [a] (-> Type Type (Check a))) @@ -337,10 +413,10 @@ (All [a] (-> (Check a) (Check a) (Check a))) (function [context] (case (left context) - (#E;Success [context' output]) - (#E;Success [context' output]) + (#e;Success [context' output]) + (#e;Success [context' output]) - (#E;Error _) + (#e;Error _) (right context)))) (def: (assumed? [e a] assumptions) @@ -357,14 +433,104 @@ (def: (on id type then else) (All [a] - (-> Nat Type (Check a) (-> Type (Check a)) + (-> Var Type (Check a) (-> Type (Check a)) (Check a))) - (either (do Monad<Check> - [_ (write id type)] - then) - (do Monad<Check> - [bound (read id)] - (else bound)))) + ($_ either + (do Monad<Check> + [_ (write type id)] + then) + (do Monad<Check> + [ring (ring id) + _ (assert "" (n.> +1 (set;size ring))) + _ (monad;map @ (update type) (set;to-list ring))] + then) + (do Monad<Check> + [bound (read id)] + (else bound)))) + +(def: (link-2 left right) + (-> Var Var (Check Unit)) + (do Monad<Check> + [_ (write (#;Var right) left)] + (write (#;Var left) right))) + +(def: (link-3 interpose to from) + (-> Var Var Var (Check Unit)) + (do Monad<Check> + [_ (update (#;Var interpose) from)] + (update (#;Var to) interpose))) + +(def: (check-vars check' assumptions idE idA) + (-> (-> Type Type Assumptions (Check Assumptions)) + Assumptions + Var Var + (Check Assumptions)) + (if (n.= idE idA) + (check/wrap assumptions) + (do Monad<Check> + [ebound (attempt (read idE)) + abound (attempt (read idA))] + (case [ebound abound] + ## Link the 2 variables circularily + [#;None #;None] + (do @ + [_ (link-2 idE idA)] + (wrap assumptions)) + + ## Interpose new variable between 2 existing links + [(#;Some etype) #;None] + (case etype + (#;Var targetE) + (do @ + [_ (link-3 idA targetE idE)] + (wrap assumptions)) + + _ + (check' etype (#;Var idA) assumptions)) + + ## Interpose new variable between 2 existing links + [#;None (#;Some atype)] + (case atype + (#;Var targetA) + (do @ + [_ (link-3 idE targetA idA)] + (wrap assumptions)) + + _ + (check' (#;Var idE) atype assumptions)) + + [(#;Some etype) (#;Some atype)] + (case [etype atype] + [(#;Var targetE) (#;Var targetA)] + (do @ + [ringE (ring idE) + ringA (ring idA)] + (if (:: set;Eq<Set> = ringE ringA) + (wrap assumptions) + ## Fuse 2 rings + (do @ + [_ (monad;fold @ (function [interpose to] + (do @ + [_ (link-3 interpose to idE)] + (wrap interpose))) + targetE + (set;to-list ringA))] + (wrap assumptions)))) + + [(#;Var targetE) _] + (do @ + [ring (ring idE) + _ (monad;map @ (update atype) (set;to-list ring))] + (wrap assumptions)) + + [_ (#;Var targetA)] + (do @ + [ring (ring idA) + _ (monad;map @ (update etype) (set;to-list ring))] + (wrap assumptions)) + + _ + (check' etype atype assumptions)))))) (def: #export (check' expected actual assumptions) {#;doc "Type-check to ensure that the 'expected' type subsumes the 'actual' type."} @@ -372,34 +538,18 @@ (if (is expected actual) (check/wrap assumptions) (case [expected actual] - [(#;Var e-id) (#;Var a-id)] - (if (n.= e-id a-id) - (check/wrap assumptions) - (do Monad<Check> - [ebound (attempt (read e-id)) - abound (attempt (read a-id))] - (case [ebound abound] - [#;None #;None] - (do @ - [_ (write e-id actual)] - (wrap assumptions)) - - [(#;Some etype) #;None] - (check' etype actual assumptions) - - [#;None (#;Some atype)] - (check' expected atype assumptions) - - [(#;Some etype) (#;Some atype)] - (check' etype atype assumptions)))) + [(#;Var idE) (#;Var idA)] + (check-vars check' assumptions idE idA) [(#;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))) @@ -529,13 +679,13 @@ {#;doc "A simple type-checking function that just returns a yes/no answer."} (-> Type Type Bool) (case (run fresh-context (check expected actual)) - (#E;Error error) + (#e;Error error) false - (#E;Success _) + (#e;Success _) true)) (def: #export get-context (Check Type-Context) (function [context] - (#E;Success [context context]))) + (#e;Success [context context]))) diff --git a/stdlib/test/test/lux/meta/type/check.lux b/stdlib/test/test/lux/meta/type/check.lux index 5fb207cec..21eed2f72 100644 --- a/stdlib/test/test/lux/meta/type/check.lux +++ b/stdlib/test/test/lux/meta/type/check.lux @@ -1,14 +1,17 @@ (;module: lux (lux [io] - (control [monad #+ do Monad]) - (data [text "text/" Monoid<Text> Eq<Text>] - text/format + (control [monad #+ do Monad] + [pipe #+ case>]) + (data [product] + [maybe] [number] - maybe - (coll [list])) + [text "text/" Monoid<Text> Eq<Text>] + text/format + (coll [list "list/" Functor<List>] + [set])) ["r" math/random] - (meta [type] + (meta [type "type/" Eq<Type>] ["@" type/check])) lux/test) @@ -162,7 +165,7 @@ (and (type-checks? (@;with (function [[id var]] (@;check var #;Unit)))) (type-checks? (@;with (function [[id var]] (@;check #;Unit var)))))) - (test "Can't rebind already bound type-vars." + (test "Cannot rebind already bound type-vars." (not (type-checks? (@;with (function [[id var]] (do @;Monad<Check> [_ (@;check var #;Unit)] @@ -180,3 +183,101 @@ [_ (@;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)) + [tail-id tail-type] (monad;fold @ (function [[tail-id tail-type] [_head-id _head-type]] + (do @ + [_ (@;check head-type tail-type)] + (wrap [tail-id tail-type]))) + [head-id head-type] + ids+types)] + (wrap [[head-id head-type] ids+types [tail-id tail-type]]))) + +(context: "Rings." + (<| (times +100) + (do @ + [num-connections (|> r;nat (:: @ map (n.% +100))) + bound (|> gen-type (r;filter (|>. (case> (#;Var _) false _ true)))) + pick-pcg (r;seq r;nat r;nat)] + ($_ seq + (test "Can create rings of variables." + (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)] + headR (@;ring head-id) + tailR (@;ring tail-id)] + (@;assert "" + (let [same-rings? (:: set;Eq<Set> = headR tailR) + expected-size? (n.= (n.inc num-connections) (set;size headR)) + same-vars? (|> (set;to-list headR) + (list;sort n.<) + (:: (list;Eq<List> number;Eq<Nat>) = (list;sort n.< (#;Cons head-id ids))))] + (and same-rings? + expected-size? + same-vars?)))))) + (test "When a var in a ring is bound, all the ring is bound." + (type-checks? (do @;Monad<Check> + [[[head-id head-type] ids+types tail-type] (build-ring num-connections) + #let [ids (list/map product;left ids+types)] + _ (@;check head-type bound) + head-bound (@;read head-id) + tail-bound (monad;map @ @;read ids) + headR (@;ring head-id) + tailR+ (monad;map @ @;ring ids)] + (let [rings-were-erased? (and (set;empty? headR) + (list;every? set;empty? tailR+)) + same-types? (list;every? (type/= bound) (list& head-bound tail-bound))] + (@;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) + [[head-idR head-typeR] ids+typesR [tail-idR tail-typeR]] (build-ring num-connections) + headRL-pre (@;ring head-idL) + headRR-pre (@;ring head-idR) + _ (@;check head-typeL head-typeR) + headRL-post (@;ring head-idL) + headRR-post (@;ring head-idR)] + (@;assert "" + (let [same-rings? (:: set;Eq<Set> = headRL-post headRR-post) + expected-size? (n.= (n.* +2 (n.inc num-connections)) + (set;size headRL-post)) + union? (:: set;Eq<Set> = headRL-post (set;union headRL-pre headRR-pre))] + (and same-rings? + expected-size? + union?)))))) + )) + )) |