aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc
diff options
context:
space:
mode:
authorEduardo Julian2017-05-20 18:29:24 -0400
committerEduardo Julian2017-05-20 18:29:24 -0400
commit8f88e4bf4b380e2f09d046fbef05fca452eae62c (patch)
tree5a8a67dae8e40cbc2586d3356268583e6eb5098d /new-luxc/source/luxc
parent76d209d7b33f713259bd9ddb453d571f814005c9 (diff)
WIP
- Added analysis and type-inference for records and tagged variants. - Extracted inference code to a separate module for better reuse.
Diffstat (limited to '')
-rw-r--r--new-luxc/source/luxc/analyser.lux7
-rw-r--r--new-luxc/source/luxc/analyser/case.lux4
-rw-r--r--new-luxc/source/luxc/analyser/function.lux108
-rw-r--r--new-luxc/source/luxc/analyser/inference.lux90
-rw-r--r--new-luxc/source/luxc/analyser/struct.lux233
5 files changed, 276 insertions, 166 deletions
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<Lux>
[[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<Lux>
[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 [<tag>]
- (<tag> left right)
- (<tag> (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 [<tag>]
- (<tag> env quantified)
- (<tag> (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<Lux>
@@ -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<Lux> 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<Lux>
- [[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<Lux>
- [[ex-id exT] (&;within-type-env
- TC;existential)]
- (analyse-apply' analyse (assume (type;apply-type funcT exT)) args))
-
- (#;Function inputT outputT)
- (do Monad<Lux>
- [[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<Lux>
- [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<Lux>
+ [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<List>]))
+ [macro #+ Monad<Lux>]
+ [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 [<tag>]
+ (<tag> left right)
+ (<tag> (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 [<tag>]
+ (<tag> env quantified)
+ (<tag> (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<Lux> 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<Lux>
+ [[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<Lux>
+ [[ex-id exT] (&;within-type-env
+ TC;existential)]
+ (apply-function analyse (assume (type;apply-type funcT exT)) args))
+
+ (#;Function inputT outputT)
+ (do Monad<Lux>
+ [[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<Lux>
+ (function [[key val]]
+ (case key
+ [_ (#;Tag key)]
+ (do Monad<Lux>
+ [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<Lux>
+ [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<Ident> (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<Nat>))
+ pairs)
+ #let [ordered-tuple (L/map (function [idx]
+ (assume (D;get idx idx->val)))
+ tuple-range)]]
+ (wrap [ordered-tuple recordT]))
+
+ _
+ (:: Monad<Lux> wrap [(list) Unit])))
+
(def: #export (analyse-tuple analyse members)
(-> &;Analyser (List Code) (Lux Analysis))
(do Monad<Lux>
@@ -118,6 +174,105 @@
(&;fail "")
))))
+(def: (record-function-type type)
+ (-> Type (Lux Type))
+ (case type
+ (#;Named name unnamedT)
+ (do Monad<Lux>
+ [unnamedT+ (record-function-type unnamedT)]
+ (wrap (#;Named name unnamedT+)))
+
+ (^template [<tag>]
+ (<tag> env bodyT)
+ (do Monad<Lux>
+ [bodyT+ (record-function-type bodyT)]
+ (wrap (<tag> env bodyT+))))
+ ([#;UnivQ]
+ [#;ExQ])
+
+ (#;Product _)
+ (:: Monad<Lux> 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<Lux>
+ [unnamedT+ (record-function-type unnamedT)]
+ (wrap (#;Named name unnamedT+)))
+
+ (^template [<tag>]
+ (<tag> env bodyT)
+ (do Monad<Lux>
+ [bodyT+ (record-function-type bodyT)]
+ (wrap (<tag> 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<Lux> 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<Lux> 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<Lux>
+ [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<Lux>
+ [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<Lux>
@@ -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<Lux>
- [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<Lux>
- (function [[key val]]
- (case key
- [_ (#;Tag key)]
- (do Monad<Lux>
- [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<Lux>
- [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<Ident> (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<Nat>))
- pairs)
- #let [ordered-tuple (L/map (function [idx]
- (assume (D;get idx idx->val)))
- tuple-range)]]
- (wrap [ordered-tuple recordT]))
-
- _
- (:: Monad<Lux> wrap [(list) Unit])))