diff options
author | Eduardo Julian | 2017-11-14 01:14:26 -0400 |
---|---|---|
committer | Eduardo Julian | 2017-11-14 01:14:26 -0400 |
commit | 290c2389bc762dfaf625d72a76a675ce15119985 (patch) | |
tree | c0eba13fc1de598b629752d2d7ab9760568fd059 /new-luxc/source/luxc/lang/analysis/inference.lux | |
parent | 530a14bfe7714f94babdb34c237b88321408a685 (diff) |
- Yet more refactoring.
Diffstat (limited to '')
-rw-r--r-- | new-luxc/source/luxc/lang/analysis/inference.lux | 80 |
1 files changed, 23 insertions, 57 deletions
diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux index 5152de0b6..8b04ac2b7 100644 --- a/new-luxc/source/luxc/lang/analysis/inference.lux +++ b/new-luxc/source/luxc/lang/analysis/inference.lux @@ -14,50 +14,22 @@ (analysis ["&;" common])))) (exception: #export Cannot-Infer) +(def: (cannot-infer type args) + (-> Type (List Code) Text) + (format " Type: " (%type type) "\n" + "Arguments:" + (|> args + list;enumerate + (list/map (function [[idx argC]] + (format "\n " (%n idx) " " (%code argC)))) + (text;join-with "")))) + (exception: #export Cannot-Infer-Argument) (exception: #export Smaller-Variant-Than-Expected) (exception: #export Invalid-Type-Application) (exception: #export Not-A-Record-Type) (exception: #export Not-A-Variant-Type) -## When doing inference, type-variables often need to be created in -## order to figure out which types are present in the expression being -## inferred. -## If a type-variable never gets bound/resolved to a type, then that -## means the expression can be generalized through universal -## quantification. -## When that happens, the type-variable must be replaced by an -## argument to the universally-quantified type. -(def: #export (replace-var var-id bound-idx type) - (-> Nat Nat Type Type) - (case type - (#;Primitive name params) - (#;Primitive name (list/map (replace-var var-id bound-idx) params)) - - (^template [<tag>] - (<tag> left right) - (<tag> (replace-var var-id bound-idx left) - (replace-var var-id bound-idx right))) - ([#;Sum] - [#;Product] - [#;Function] - [#;Apply]) - - (#;Var id) - (if (n.= var-id id) - (#;Bound bound-idx) - type) - - (^template [<tag>] - (<tag> env quantified) - (<tag> (list/map (replace-var var-id bound-idx) env) - (replace-var var-id (n.+ +2 bound-idx) quantified))) - ([#;UnivQ] - [#;ExQ]) - - _ - type)) - (def: (replace-bound bound-idx replacementT type) (-> Nat Type Type Type) (case type @@ -110,18 +82,8 @@ (#;UnivQ _) (do meta;Monad<Meta> - [[var-id varT] (&;with-type-env tc;var) - [outputT argsA] (general analyse (maybe;assume (type;apply (list varT) inferT)) args)] - (do @ - [? (&;with-type-env - (tc;concrete? var-id)) - ## Quantify over the type if genericity/parametricity - ## is discovered. - outputT' (if ? - (&;with-type-env - (tc;clean var-id outputT)) - (wrap (type;univ-q +1 (replace-var var-id +1 outputT))))] - (wrap [outputT' argsA]))) + [[var-id varT] (&;with-type-env tc;var)] + (general analyse (maybe;assume (type;apply (list varT) inferT)) args)) (#;ExQ _) (do meta;Monad<Meta> @@ -155,14 +117,18 @@ (analyse argC)))] (wrap [outputT' (list& argA args'A)])) + (#;Var infer-id) + (do meta;Monad<Meta> + [?inferT' (&;with-type-env (tc;read infer-id))] + (case ?inferT' + (#;Some inferT') + (general analyse inferT' args) + + _ + (&;throw Cannot-Infer (cannot-infer inferT args)))) + _ - (&;throw Cannot-Infer (format " Type: " (%type inferT) "\n" - "Arguments:" - (|> args - list;enumerate - (list/map (function [[idx argC]] - (format "\n " (%n idx) " " (%code argC)))) - (text;join-with ""))))) + (&;throw Cannot-Infer (cannot-infer inferT args))) )) ## Turns a record type into the kind of function type suitable for inference. |