From 15121222d570f8fe3c5a326208e4f0bad737e63c Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Tue, 31 Oct 2017 23:39:49 -0400 Subject: - Re-organized analysis. --- new-luxc/source/luxc/lang/analysis/inference.lux | 228 +++++++++++++++++++++++ 1 file changed, 228 insertions(+) create mode 100644 new-luxc/source/luxc/lang/analysis/inference.lux (limited to 'new-luxc/source/luxc/lang/analysis/inference.lux') diff --git a/new-luxc/source/luxc/lang/analysis/inference.lux b/new-luxc/source/luxc/lang/analysis/inference.lux new file mode 100644 index 000000000..cd484a623 --- /dev/null +++ b/new-luxc/source/luxc/lang/analysis/inference.lux @@ -0,0 +1,228 @@ +(;module: + lux + (lux (control [monad #+ do] + ["ex" exception #+ exception:]) + (data [maybe] + [text] + text/format + (coll [list "list/" Functor])) + [meta #+ Monad] + (meta [type] + (type ["tc" check]))) + (luxc ["&" base] + (lang ["la" analysis #+ Analysis] + (analysis ["&;" common])))) + +(exception: #export Cannot-Infer) +(exception: #export Cannot-Infer-Argument) +(exception: #export Smaller-Variant-Than-Expected) + +## 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 [] + ( left right) + ( (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 [] + ( env quantified) + ( (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 + (#;Primitive name params) + (#;Primitive name (list/map (replace-bound bound-idx replacementT) params)) + + (^template [] + ( left right) + ( (replace-bound bound-idx replacementT left) + (replace-bound bound-idx replacementT right))) + ([#;Sum] + [#;Product] + [#;Function] + [#;Apply]) + + (#;Bound idx) + (if (n.= bound-idx idx) + replacementT + type) + + (^template [] + ( env quantified) + ( (list/map (replace-bound bound-idx replacementT) env) + (replace-bound (n.+ +2 bound-idx) replacementT quantified))) + ([#;UnivQ] + [#;ExQ]) + + _ + type)) + +## Type-inference works by applying some (potentially quantified) type +## to a sequence of values. +## Function types are used for this, although inference is not always +## done for function application (alternative uses may be records and +## tagged variants). +## But, so long as the type being used for the inference can be trated +## as a function type, this method of inference should work. +(def: #export (apply-function analyse funcT args) + (-> &;Analyser Type (List Code) (Meta [Type (List Analysis)])) + (case args + #;Nil + (:: Monad wrap [funcT (list)]) + + (#;Cons argC args') + (case funcT + (#;Named name unnamedT) + (apply-function analyse unnamedT args) + + (#;UnivQ _) + (&common;with-var + (function [[var-id varT]] + (do Monad + [[outputT argsA] (apply-function analyse (maybe;assume (type;apply (list varT) funcT)) args)] + (do @ + [? (&;with-type-env + (tc;bound? 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]))))) + + (#;ExQ _) + (do Monad + [[ex-id exT] (&;with-type-env + tc;existential)] + (apply-function analyse (maybe;assume (type;apply (list exT) funcT)) args)) + + ## Arguments are inferred back-to-front because, by convention, + ## Lux functions take the most important arguments *last*, which + ## means that the most information for doing proper inference is + ## located in the last arguments to a function call. + ## By inferring back-to-front, a lot of type-annotations can be + ## avoided in Lux code, since the inference algorithm can piece + ## things together more easily. + (#;Function inputT outputT) + (do Monad + [[outputT' args'A] (apply-function analyse outputT args') + argA (&;with-stacked-errors + (function [_] (Cannot-Infer-Argument + (format "Inferred Type: " (%type inputT) "\n" + " Argument: " (%code argC)))) + (&;with-expected-type inputT + (analyse argC)))] + (wrap [outputT' (list& argA args'A)])) + + _ + (&;throw Cannot-Infer (format "Inference Type: " (%type funcT) + " Arguments: " (|> args (list/map %code) (text;join-with " "))))) + )) + +## Turns a record type into the kind of function type suitable for inference. +(def: #export (record type) + (-> Type (Meta Type)) + (case type + (#;Named name unnamedT) + (do Monad + [unnamedT+ (record unnamedT)] + (wrap unnamedT+)) + + (^template [] + ( env bodyT) + (do Monad + [bodyT+ (record bodyT)] + (wrap ( env bodyT+)))) + ([#;UnivQ] + [#;ExQ]) + + (#;Product _) + (:: Monad wrap (type;function (type;flatten-tuple type) type)) + + _ + (&;fail (format "Not a record type: " (%type type))))) + +## Turns a variant type into the kind of function type suitable for inference. +(def: #export (variant tag expected-size type) + (-> Nat Nat Type (Meta Type)) + (loop [depth +0 + currentT type] + (case currentT + (#;Named name unnamedT) + (do Monad + [unnamedT+ (recur depth unnamedT)] + (wrap unnamedT+)) + + (^template [] + ( env bodyT) + (do Monad + [bodyT+ (recur (n.inc depth) bodyT)] + (wrap ( env bodyT+)))) + ([#;UnivQ] + [#;ExQ]) + + (#;Sum _) + (let [cases (type;flatten-variant currentT) + actual-size (list;size cases) + boundary (n.dec expected-size)] + (cond (or (n.= expected-size actual-size) + (and (n.> expected-size actual-size) + (n.< boundary tag))) + (case (list;nth tag cases) + (#;Some caseT) + (:: Monad wrap (if (n.= +0 depth) + (type;function (list caseT) currentT) + (let [replace! (replace-bound (|> depth n.dec (n.* +2)) type)] + (type;function (list (replace! caseT)) + (replace! currentT))))) + + #;None + (&common;variant-out-of-bounds-error type expected-size tag)) + + (n.< expected-size actual-size) + (&;throw Smaller-Variant-Than-Expected + (format "Expected: " (%i (nat-to-int expected-size)) "\n" + " Actual: " (%i (nat-to-int actual-size)))) + + (n.= boundary tag) + (let [caseT (type;variant (list;drop boundary cases))] + (:: Monad wrap (if (n.= +0 depth) + (type;function (list caseT) currentT) + (let [replace! (replace-bound (|> depth n.dec (n.* +2)) type)] + (type;function (list (replace! caseT)) + (replace! currentT)))))) + + ## else + (&common;variant-out-of-bounds-error type expected-size tag))) + + _ + (&;fail (format "Not a variant type: " (%type type)))))) -- cgit v1.2.3