From 8f88e4bf4b380e2f09d046fbef05fca452eae62c Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Sat, 20 May 2017 18:29:24 -0400 Subject: WIP - Added analysis and type-inference for records and tagged variants. - Extracted inference code to a separate module for better reuse. --- new-luxc/source/luxc/analyser.lux | 7 + new-luxc/source/luxc/analyser/case.lux | 4 +- new-luxc/source/luxc/analyser/function.lux | 108 ++----------- new-luxc/source/luxc/analyser/inference.lux | 90 +++++++++++ new-luxc/source/luxc/analyser/struct.lux | 233 +++++++++++++++++++--------- 5 files changed, 276 insertions(+), 166 deletions(-) create mode 100644 new-luxc/source/luxc/analyser/inference.lux (limited to 'new-luxc/source/luxc') diff --git a/new-luxc/source/luxc/analyser.lux b/new-luxc/source/luxc/analyser.lux index d8f5abe9b..90140afb4 100644 --- a/new-luxc/source/luxc/analyser.lux +++ b/new-luxc/source/luxc/analyser.lux @@ -63,6 +63,9 @@ (^ (#;Tuple elems)) (&&struct;analyse-tuple analyse elems) + (^ (#;Record pairs)) + (&&struct;analyse-record analyse pairs) + (#;Symbol reference) (&&reference;analyse-reference reference) @@ -92,6 +95,10 @@ value))) (&&struct;analyse-variant analyse tag value) + (^ (#;Form (list [_ (#;Tag tag)] + value))) + (&&struct;analyse-tagged-variant analyse tag value) + (^ (#;Form (list& func args))) (do Monad [[funcT =func] (&&common;with-unknown-type diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux index 391261ac8..ee009b1ab 100644 --- a/new-luxc/source/luxc/analyser/case.lux +++ b/new-luxc/source/luxc/analyser/case.lux @@ -192,9 +192,9 @@ (&;with-cursor cursor (do Monad [tag (macro;normalize tag) - [idx group tagT] (macro;resolve-tag tag) + [idx group variantT] (macro;resolve-tag tag) _ (&;within-type-env - (TC;check inputT tagT))] + (TC;check inputT variantT))] (analyse-pattern (#;Some (list;size group)) inputT (' ((~ (code;nat idx)) (~@ values))) next))) _ diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux index 44deec45b..838de4181 100644 --- a/new-luxc/source/luxc/analyser/function.lux +++ b/new-luxc/source/luxc/analyser/function.lux @@ -10,43 +10,10 @@ (luxc ["&" base] (lang ["la" analysis #+ Analysis]) ["&;" env] - (analyser ["&;" common]))) + (analyser ["&;" common] + ["&;" inference]))) ## [Analysers] -(def: (bind-var var-id bound-idx type) - (-> Nat Nat Type Type) - (case type - (#;Host name params) - (#;Host name (L/map (bind-var var-id bound-idx) params)) - - (^template [] - ( left right) - ( (bind-var var-id bound-idx left) - (bind-var var-id bound-idx right))) - ([#;Sum] - [#;Product] - [#;Function] - [#;App]) - - (#;Var id) - (if (n.= var-id id) - (#;Bound bound-idx) - type) - - (^template [] - ( env quantified) - ( (L/map (bind-var var-id bound-idx) env) - (bind-var var-id (n.+ +2 bound-idx) quantified))) - ([#;UnivQ] - [#;ExQ]) - - (#;Named name unnamedT) - (#;Named name - (bind-var var-id bound-idx unnamedT)) - - _ - type)) - (def: #export (analyse-function analyse func-name arg-name body) (-> &;Analyser Text Text Code (Lux Analysis)) (do Monad @@ -103,7 +70,7 @@ funT'' (if concrete-input? (&;within-type-env (TC;clean input-id funT')) - (wrap (#;UnivQ (list) (bind-var input-id +1 funT')))) + (wrap (#;UnivQ (list) (&inference;bind-var input-id +1 funT')))) _ (&;within-type-env (TC;check expected funT''))] (wrap =function)) @@ -121,62 +88,17 @@ (&;fail "") ))))) -(def: (analyse-apply' analyse funcT args) - (-> &;Analyser Type (List Code) (Lux [Type (List Analysis)])) - (case args - #;Nil - (:: Monad wrap [funcT (list)]) - - (#;Cons arg args') - (&;with-stacked-errors - (function [_] (format "Cannot apply function " (%type funcT) - " to args: " (|> args (L/map %code) (text;join-with " ")))) - (case funcT - (#;Named name unnamedT) - (analyse-apply' analyse unnamedT args) - - (#;UnivQ _) - (&common;with-var - (function [[var-id varT]] - (do Monad - [[outputT argsA] (analyse-apply' analyse (assume (type;apply-type funcT varT)) args)] - (do @ - [? (&;within-type-env - (TC;bound? var-id)) - outputT' (if ? - (&;within-type-env - (TC;clean var-id outputT)) - (wrap (#;UnivQ (list) (bind-var var-id +1 outputT))))] - (wrap [outputT' argsA]))))) - - (#;ExQ _) - (do Monad - [[ex-id exT] (&;within-type-env - TC;existential)] - (analyse-apply' analyse (assume (type;apply-type funcT exT)) args)) - - (#;Function inputT outputT) - (do Monad - [[outputT' args'A] (analyse-apply' analyse outputT args') - argA (&;with-stacked-errors - (function [_] (format "Expected type: " (%type inputT) "\n" - " For argument: " (%code arg))) - (&;with-expected-type inputT - (analyse arg)))] - (wrap [outputT' (list& argA args'A)])) - - _ - (&;fail (format "Cannot apply a non-function: " (%type funcT))))) - )) - (def: #export (analyse-apply analyse funcT funcA args) (-> &;Analyser Type Analysis (List Code) (Lux Analysis)) - (do Monad - [expected macro;expected-type - [applyT argsA] (analyse-apply' analyse funcT args) - _ (&;within-type-env - (TC;check expected applyT))] - (wrap (L/fold (function [arg func] - (#la;Apply arg func)) - funcA - argsA)))) + (&;with-stacked-errors + (function [_] (format "Cannot apply function " (%type funcT) + " to args: " (|> args (L/map %code) (text;join-with " ")))) + (do Monad + [expected macro;expected-type + [applyT argsA] (&inference;apply-function analyse funcT args) + _ (&;within-type-env + (TC;check expected applyT))] + (wrap (L/fold (function [arg func] + (#la;Apply arg func)) + funcA + argsA))))) diff --git a/new-luxc/source/luxc/analyser/inference.lux b/new-luxc/source/luxc/analyser/inference.lux new file mode 100644 index 000000000..824071ab3 --- /dev/null +++ b/new-luxc/source/luxc/analyser/inference.lux @@ -0,0 +1,90 @@ +(;module: + lux + (lux (control monad) + (data text/format + (coll [list "L/" Functor])) + [macro #+ Monad] + [type] + (type ["TC" check])) + (luxc ["&" base] + (lang ["la" analysis #+ Analysis]) + (analyser ["&;" common]))) + +(def: #export (bind-var var-id bound-idx type) + (-> Nat Nat Type Type) + (case type + (#;Host name params) + (#;Host name (L/map (bind-var var-id bound-idx) params)) + + (^template [] + ( left right) + ( (bind-var var-id bound-idx left) + (bind-var var-id bound-idx right))) + ([#;Sum] + [#;Product] + [#;Function] + [#;App]) + + (#;Var id) + (if (n.= var-id id) + (#;Bound bound-idx) + type) + + (^template [] + ( env quantified) + ( (L/map (bind-var var-id bound-idx) env) + (bind-var var-id (n.+ +2 bound-idx) quantified))) + ([#;UnivQ] + [#;ExQ]) + + (#;Named name unnamedT) + (#;Named name + (bind-var var-id bound-idx unnamedT)) + + _ + type)) + +(def: #export (apply-function analyse funcT args) + (-> &;Analyser Type (List Code) (Lux [Type (List Analysis)])) + (case args + #;Nil + (:: Monad wrap [funcT (list)]) + + (#;Cons arg 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 (assume (type;apply-type funcT varT)) args)] + (do @ + [? (&;within-type-env + (TC;bound? var-id)) + outputT' (if ? + (&;within-type-env + (TC;clean var-id outputT)) + (wrap (#;UnivQ (list) (bind-var var-id +1 outputT))))] + (wrap [outputT' argsA]))))) + + (#;ExQ _) + (do Monad + [[ex-id exT] (&;within-type-env + TC;existential)] + (apply-function analyse (assume (type;apply-type funcT exT)) args)) + + (#;Function inputT outputT) + (do Monad + [[outputT' args'A] (apply-function analyse outputT args') + argA (&;with-stacked-errors + (function [_] (format "Expected type: " (%type inputT) "\n" + " For argument: " (%code arg))) + (&;with-expected-type inputT + (analyse arg)))] + (wrap [outputT' (list& argA args'A)])) + + _ + (&;fail (format "Cannot apply a non-function: " (%type funcT)))) + )) diff --git a/new-luxc/source/luxc/analyser/struct.lux b/new-luxc/source/luxc/analyser/struct.lux index c1b332155..185b8747f 100644 --- a/new-luxc/source/luxc/analyser/struct.lux +++ b/new-luxc/source/luxc/analyser/struct.lux @@ -20,7 +20,8 @@ (lang ["la" analysis #+ Analysis]) ["&;" module] ["&;" env] - (analyser ["&;" common]))) + (analyser ["&;" common] + ["&;" inference]))) ## [Analysers] (def: (analyse-typed-tuple analyse members) @@ -69,6 +70,61 @@ (wrap (#la;Tuple (L/append =prevs (list =last))))) )))) +(def: #export (normalize-record pairs) + (-> (List [Code Code]) (Lux (List [Ident Code]))) + (mapM Monad + (function [[key val]] + (case key + [_ (#;Tag key)] + (do Monad + [key (macro;normalize key)] + (wrap [key val])) + + _ + (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key))))) + pairs)) + +(def: #export (order-record pairs) + (-> (List [Ident Code]) (Lux [(List Code) Type])) + (case pairs + (#;Cons [head-k head-v] _) + (do Monad + [head-k (macro;normalize head-k) + [_ tag-set recordT] (macro;resolve-tag head-k) + #let [size-record (list;size pairs) + size-ts (list;size tag-set)] + _ (if (n.= size-ts size-record) + (wrap []) + (&;fail (format "Record size does not match tag-set size." "\n" + "Expected: " (|> size-ts nat-to-int %i) "\n" + " Actual: " (|> size-record nat-to-int %i) "\n" + "For type: " (%type recordT)))) + #let [tuple-range (list;n.range +0 size-ts) + tag->idx (D;from-list ident;Hash (list;zip2 tag-set tuple-range))] + idx->val (foldM @ + (function [[key val] idx->val] + (do @ + [key (macro;normalize key)] + (case (D;get key tag->idx) + #;None + (&;fail (format "Tag " (%code (code;tag key)) + " does not belong to tag-set for type " (%type recordT))) + + (#;Some idx) + (if (D;contains? idx idx->val) + (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key)))) + (wrap (D;put idx val idx->val)))))) + (: (D;Dict Nat Code) + (D;new number;Hash)) + pairs) + #let [ordered-tuple (L/map (function [idx] + (assume (D;get idx idx->val))) + tuple-range)]] + (wrap [ordered-tuple recordT])) + + _ + (:: Monad wrap [(list) Unit]))) + (def: #export (analyse-tuple analyse members) (-> &;Analyser (List Code) (Lux Analysis)) (do Monad @@ -118,6 +174,105 @@ (&;fail "") )))) +(def: (record-function-type type) + (-> Type (Lux Type)) + (case type + (#;Named name unnamedT) + (do Monad + [unnamedT+ (record-function-type unnamedT)] + (wrap (#;Named name unnamedT+))) + + (^template [] + ( env bodyT) + (do Monad + [bodyT+ (record-function-type bodyT)] + (wrap ( env bodyT+)))) + ([#;UnivQ] + [#;ExQ]) + + (#;Product _) + (:: Monad wrap (type;function (type;flatten-tuple type) type)) + + _ + (&;fail (format "Not a record type: " (%type type))))) + +(def: (out-of-bounds-error type size tag) + (All [a] (-> Type Nat Nat (Lux a))) + (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n" + " Tag: " (%i (nat-to-int tag)) "\n" + "Size: " (%i (nat-to-int size)) "\n" + "Type: " (%type type)))) + +(def: (variant-function-type tag expected-size type) + (-> Nat Nat Type (Lux Type)) + (case type + (#;Named name unnamedT) + (do Monad + [unnamedT+ (record-function-type unnamedT)] + (wrap (#;Named name unnamedT+))) + + (^template [] + ( env bodyT) + (do Monad + [bodyT+ (record-function-type bodyT)] + (wrap ( env bodyT+)))) + ([#;UnivQ] + [#;ExQ]) + + (#;Sum _) + (let [cases (type;flatten-variant type) + 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 (type;function (list caseT) type)) + + #;None + (out-of-bounds-error type expected-size tag)) + + (n.< expected-size actual-size) + (&;fail (format "Variant type is smaller than expected." "\n" + "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 (type;function (list caseT) type))) + + ## else + (out-of-bounds-error type expected-size tag))) + + _ + (&;fail (format "Not a variant type: " (%type type))))) + +(def: #export (analyse-record analyse members) + (-> &;Analyser (List [Code Code]) (Lux Analysis)) + (do Monad + [members (normalize-record members) + [members recordT] (order-record members) + expectedT macro;expected-type + functionT (record-function-type recordT) + [inferredT membersA] (&inference;apply-function analyse functionT members) + _ (&;within-type-env + (TC;check expectedT inferredT))] + (wrap (#la;Tuple membersA)))) + +(def: #export (analyse-tagged-variant analyse tag value) + (-> &;Analyser Ident Code (Lux Analysis)) + (do Monad + [tag (macro;normalize tag) + [idx group variantT] (macro;resolve-tag tag) + #let [case-size (list;size group)] + functionT (variant-function-type idx case-size variantT) + [inferredT valueA+] (&inference;apply-function analyse functionT (list value)) + expectedT macro;expected-type + _ (&;within-type-env + (TC;check expectedT inferredT))] + (wrap (#la;Variant idx case-size (|> valueA+ list;head assume))))) + (def: #export (analyse-variant analyse tag value) (-> &;Analyser Nat Code (Lux Analysis)) (do Monad @@ -128,17 +283,15 @@ (#;Sum _) (let [flat (type;flatten-variant expected) type-size (list;size flat)] - (if (n.< type-size tag) + (case (list;nth tag flat) + (#;Some variant-type) (do @ - [#let [variant-type (default (undefined) - (list;nth tag flat))] - =value (&;with-expected-type variant-type + [=value (&;with-expected-type variant-type (analyse value))] (wrap (#la;Variant tag type-size =value))) - (&;fail (format "Trying to create variant with tag beyond type's limitations." "\n" - " Tag: " (%n tag) "\n" - "Type size: " (%n type-size) "\n" - " Type: " (%type expected) "\n")))) + + #;None + (out-of-bounds-error expected type-size tag))) (#;Named name unnamedT) (&;with-expected-type unnamedT @@ -171,65 +324,3 @@ _ (&;fail ""))))) - -(def: (resolve-pair [key val]) - (-> [Ident Code] (Lux [Type Nat Code])) - (do Monad - [key (macro;normalize key) - [idx tag-set recordT] (macro;resolve-tag key)] - (wrap [recordT idx val]))) - -(def: #export (normalize-record pairs) - (-> (List [Code Code]) (Lux (List [Ident Code]))) - (mapM Monad - (function [[key val]] - (case key - [_ (#;Tag key)] - (do Monad - [key (macro;normalize key)] - (wrap [key val])) - - _ - (&;fail (format "Cannot use non-tag tokens in key positions in records: " (%code key))))) - pairs)) - -(def: #export (order-record pairs) - (-> (List [Ident Code]) (Lux [(List Code) Type])) - (case pairs - (#;Cons [head-k head-v] _) - (do Monad - [head-k (macro;normalize head-k) - [_ tag-set recordT] (macro;resolve-tag head-k) - #let [size-record (list;size pairs) - size-ts (list;size tag-set)] - _ (if (n.= size-ts size-record) - (wrap []) - (&;fail (format "Record size does not match tag-set size." "\n" - "Expected: " (|> size-ts nat-to-int %i) "\n" - " Actual: " (|> size-record nat-to-int %i) "\n" - "For type: " (%type recordT)))) - #let [tuple-range (list;n.range +0 size-ts) - tag->idx (D;from-list ident;Hash (list;zip2 tag-set tuple-range))] - idx->val (foldM @ - (function [[key val] idx->val] - (do @ - [key (macro;normalize key)] - (case (D;get key tag->idx) - #;None - (&;fail (format "Tag " (%code (code;tag key)) - " does not belong to tag-set for type " (%type recordT))) - - (#;Some idx) - (if (D;contains? idx idx->val) - (&;fail (format "Cannot repeat tag inside record: " (%code (code;tag key)))) - (wrap (D;put idx val idx->val)))))) - (: (D;Dict Nat Code) - (D;new number;Hash)) - pairs) - #let [ordered-tuple (L/map (function [idx] - (assume (D;get idx idx->val))) - tuple-range)]] - (wrap [ordered-tuple recordT])) - - _ - (:: Monad wrap [(list) Unit]))) -- cgit v1.2.3