diff options
| -rw-r--r-- | stdlib/source/lux/type/check.lux | 106 |
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 _) |