diff options
| -rw-r--r-- | new-luxc/source/luxc/analyser/function.lux | 24 | ||||
| -rw-r--r-- | stdlib/source/lux/meta/type/check.lux | 51 |
2 files changed, 43 insertions, 32 deletions
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux index 424a3188f..1432308f8 100644 --- a/new-luxc/source/luxc/analyser/function.lux +++ b/new-luxc/source/luxc/analyser/function.lux @@ -19,10 +19,10 @@ (-> &;Analyser Text Text Code (Meta Analysis)) (do Monad<Meta> [functionT meta;expected-type] - (loop [expected functionT] + (loop [expectedT functionT] (&;with-stacked-errors - (function [_] (format "Functions require function types: " (type;to-text expected))) - (case expected + (function [_] (format "Functions require function types: " (type;to-text expectedT))) + (case expectedT (#;Named name unnamedT) (recur unnamedT) @@ -38,22 +38,22 @@ (do @ [[var-id var] (&;with-type-env tc;existential)] - (recur (maybe;assume (type;apply (list var) expected)))) + (recur (maybe;assume (type;apply (list var) expectedT)))) (#;ExQ _) (&common;with-var (function [[var-id var]] - (recur (maybe;assume (type;apply (list var) expected))))) + (recur (maybe;assume (type;apply (list var) expectedT))))) (#;Var id) (do @ [? (&;with-type-env - (tc;bound? id))] + (tc;concrete? id))] (if ? (do @ - [expected' (&;with-type-env - (tc;read id))] - (recur expected')) + [expectedT' (&;with-type-env + (tc;read id))] + (recur expectedT')) ## Inference (&common;with-var (function [[input-id inputT]] @@ -65,13 +65,13 @@ funT' (&;with-type-env (tc;clean output-id funT)) concrete-input? (&;with-type-env - (tc;bound? input-id)) + (tc;concrete? input-id)) funT'' (if concrete-input? (&;with-type-env (tc;clean input-id funT')) (wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT')))) _ (&;with-type-env - (tc;check expected funT''))] + (tc;check expectedT funT''))] (wrap funA)) )))))) @@ -80,7 +80,7 @@ &;with-scope ## Functions have access not only to their argument, but ## also to themselves, through a local variable. - (&scope;with-local [func-name functionT]) + (&scope;with-local [func-name expectedT]) (&scope;with-local [arg-name inputT]) (&;with-expected-type outputT) (analyse body)) diff --git a/stdlib/source/lux/meta/type/check.lux b/stdlib/source/lux/meta/type/check.lux index 920eb876c..0fa56b600 100644 --- a/stdlib/source/lux/meta/type/check.lux +++ b/stdlib/source/lux/meta/type/check.lux @@ -157,7 +157,7 @@ (-> Var (Check Bool)) (function [context] (case (|> context (get@ #;var-bindings) (var::get id)) - (#;Some (#;Some _)) + (#;Some (#;Some bound)) (#e;Success [context true]) (#;Some #;None) @@ -166,6 +166,19 @@ #;None (ex;throw Unknown-Type-Var (nat/encode id))))) +(def: #export (concrete? id) + (-> Var (Check Bool)) + (function [context] + (case (|> context (get@ #;var-bindings) (var::get id)) + (#;Some (#;Some bound)) + (#e;Success [context (case bound (#;Var _) false _ true)]) + + (#;Some #;None) + (#e;Success [context false]) + + #;None + (ex;throw Unknown-Type-Var (nat/encode id))))) + (def: #export (read id) (-> Var (Check Type)) (function [context] @@ -215,6 +228,13 @@ #;None (ex;throw Unknown-Type-Var (nat/encode id))))) +(def: #export (throw exception message) + (All [a] (-> ex;Exception Text (Check a))) + (function [context] + (ex;throw exception message))) + +(exception: #export Cannot-Clean-Unbound-Var) + (def: #export (clean t-id type) (-> Var Type (Check Type)) (case type @@ -224,27 +244,15 @@ [? (bound? id)] (if ? (read id) - (wrap type))) + (throw Cannot-Clean-Unbound-Var (type;to-text type)))) (do Monad<Check> - [? (bound? id)] + [? (concrete? id)] (if ? (do Monad<Check> [=type (read id) - ==type (clean t-id =type)] - (case ==type - (#;Var =id) - (if (n.= t-id =id) - (do Monad<Check> - [_ (clear id)] - (wrap type)) - (do Monad<Check> - [_ (update ==type id)] - (wrap type))) - - _ - (do Monad<Check> - [_ (update ==type id)] - (wrap type)))) + ==type (clean t-id =type) + _ (update ==type id)] + (wrap type)) (wrap type)))) (#;Primitive name params) @@ -355,7 +363,8 @@ (def: #export (delete id) (-> Var (Check Unit)) (do Monad<Check> - [?link (pre-link id)] + [_ (wrap []) + ?link (pre-link id)] (case ?link #;None (delete' id) @@ -363,7 +372,9 @@ (#;Some pre) (do @ [post (read id) - _ (update post pre)] + _ (if (type/= (#;Var pre) post) + (clear pre) + (update post pre))] (delete' id))))) (def: #export (with k) |