aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/source/luxc/analyser
diff options
context:
space:
mode:
authorEduardo Julian2017-05-19 23:54:16 -0400
committerEduardo Julian2017-05-19 23:54:16 -0400
commitb81f241bd90092f52a47f64f4dc8297cc4f82f56 (patch)
treea07f20ec91597ca98e66833e14c42accf6b169f7 /new-luxc/source/luxc/analyser
parenta73037f8ab46e31196b1257d7621ceeacb1cad38 (diff)
- WIP: Added pattern-matching (case) analysis.
Diffstat (limited to 'new-luxc/source/luxc/analyser')
-rw-r--r--new-luxc/source/luxc/analyser/case.lux448
-rw-r--r--new-luxc/source/luxc/analyser/function.lux137
-rw-r--r--new-luxc/source/luxc/analyser/pattern.lux3
-rw-r--r--new-luxc/source/luxc/analyser/struct.lux67
4 files changed, 580 insertions, 75 deletions
diff --git a/new-luxc/source/luxc/analyser/case.lux b/new-luxc/source/luxc/analyser/case.lux
new file mode 100644
index 000000000..fc151f771
--- /dev/null
+++ b/new-luxc/source/luxc/analyser/case.lux
@@ -0,0 +1,448 @@
+(;module:
+ lux
+ (lux (control monad
+ eq)
+ (data [bool "B/" Eq<Bool>]
+ [number]
+ [char]
+ [text]
+ text/format
+ [product]
+ ["R" result "R/" Monad<Result>]
+ (coll [list "L/" Fold<List> Monoid<List> Monad<List>]
+ ["D" dict]))
+ [macro #+ Monad<Lux>]
+ (macro [code])
+ [type]
+ (type ["TC" check]))
+ (luxc ["&" base]
+ (lang ["la" analysis #+ Analysis]
+ ["lp" pattern #+ Pattern])
+ ["&;" env]
+ (analyser ["&;" common]
+ ["&;" struct])))
+
+(type: #rec Coverage
+ #PartialC
+ (#BoolC Bool)
+ (#VariantC Nat (D;Dict Nat Coverage))
+ (#SeqC Coverage Coverage)
+ (#AltC Coverage Coverage)
+ #TotalC)
+
+(def: (pattern-error type pattern)
+ (-> Type Code Text)
+ (format "Cannot match this type: " (%type type) "\n"
+ " With this pattern: " (%code pattern)))
+
+(def: (simplify-case-type type)
+ (-> Type (Lux Type))
+ (case type
+ (#;Var id)
+ (do Monad<Lux>
+ [? (&;within-type-env
+ (TC;bound? id))]
+ (if ?
+ (do @
+ [type' (&;within-type-env
+ (TC;read-var id))]
+ (simplify-case-type type'))
+ (&;fail (format "Cannot simplify type for pattern-matching: " (%type type)))))
+
+ (#;Named name unnamedT)
+ (simplify-case-type unnamedT)
+
+ (^or (#;UnivQ _) (#;ExQ _))
+ (do Monad<Lux>
+ [[ex-id exT] (&;within-type-env
+ TC;existential)]
+ (simplify-case-type (assume (type;apply-type type exT))))
+
+ _
+ (:: Monad<Lux> wrap type)))
+
+(def: (analyse-pattern num-tags inputT pattern next)
+ (All [a] (-> (Maybe Nat) Type Code (Lux a) (Lux [Pattern a])))
+ (case pattern
+ [cursor (#;Symbol ["" name])]
+ (&;with-cursor cursor
+ (do Monad<Lux>
+ [outputA (&env;with-local [name inputT]
+ next)
+ idx &env;next-local]
+ (wrap [(#lp;Bind idx) outputA])))
+
+ [cursor (#;Symbol ident)]
+ (&;with-cursor cursor
+ (&;fail (format "Symbols must be unqualified inside patterns: " (%ident ident))))
+
+ (^template [<type> <code-tag> <pattern-tag>]
+ [cursor (<code-tag> test)]
+ (&;with-cursor cursor
+ (do Monad<Lux>
+ [_ (&;within-type-env
+ (TC;check inputT <type>))
+ outputA next]
+ (wrap [(<pattern-tag> test) outputA]))))
+ ([Bool #;Bool #lp;Bool]
+ [Nat #;Nat #lp;Nat]
+ [Int #;Int #lp;Int]
+ [Deg #;Deg #lp;Deg]
+ [Real #;Real #lp;Real]
+ [Char #;Char #lp;Char]
+ [Text #;Text #lp;Text])
+
+ (^ [cursor (#;Tuple (list))])
+ (&;with-cursor cursor
+ (do Monad<Lux>
+ [_ (&;within-type-env
+ (TC;check inputT Unit))
+ outputA next]
+ (wrap [#lp;Unit outputA])))
+
+ (^ [cursor (#;Tuple (list singleton))])
+ (analyse-pattern #;None inputT singleton next)
+
+ [cursor (#;Tuple sub-patterns)]
+ (&;with-cursor cursor
+ (do Monad<Lux>
+ [inputT' (simplify-case-type inputT)]
+ (case inputT'
+ (#;Product _)
+ (let [sub-types (type;flatten-tuple inputT)
+ num-sub-types (default (list;size sub-types)
+ num-tags)
+ num-sub-patterns (list;size sub-patterns)
+ matches (cond (n.< num-sub-types num-sub-patterns)
+ (let [[prefix suffix] (list;split (n.dec num-sub-patterns) sub-types)]
+ (list;zip2 (L/append prefix (list (type;tuple suffix))) sub-patterns))
+
+ (n.> num-sub-types num-sub-patterns)
+ (let [[prefix suffix] (list;split (n.dec num-sub-types) sub-patterns)]
+ (list;zip2 sub-types (L/append prefix (list (code;tuple suffix)))))
+
+ ## (n.= num-sub-types num-sub-patterns)
+ (list;zip2 sub-types sub-patterns)
+ )]
+ (do @
+ [[memberP+ thenA] (L/fold (: (All [a]
+ (-> [Type Code] (Lux [(List Pattern) a])
+ (Lux [(List Pattern) a])))
+ (function [[memberT memberC] then]
+ (do @
+ [[memberP [memberP+ thenA]] ((:! (All [a] (-> (Maybe Nat) Type Code (Lux a) (Lux [Pattern a])))
+ analyse-pattern)
+ #;None memberT memberC then)]
+ (wrap [(list& memberP memberP+) thenA]))))
+ (do @
+ [nextA next]
+ (wrap [(list) nextA]))
+ matches)]
+ (wrap [(#lp;Tuple memberP+) thenA])))
+
+ _
+ (&;fail (pattern-error inputT pattern))
+ )))
+
+ [cursor (#;Record pairs)]
+ (do Monad<Lux>
+ [pairs (&struct;normalize-record pairs)
+ [members recordT] (&struct;order-record pairs)
+ _ (&;within-type-env
+ (TC;check inputT recordT))]
+ (analyse-pattern (#;Some (list;size members)) inputT [cursor (#;Tuple members)] next))
+
+ [cursor (#;Tag tag)]
+ (&;with-cursor cursor
+ (analyse-pattern #;None inputT (` ((~ pattern))) next))
+
+ (^ [cursor (#;Form (list& [_ (#;Nat idx)] values))])
+ (&;with-cursor cursor
+ (do Monad<Lux>
+ [inputT' (simplify-case-type inputT)]
+ (case inputT'
+ (#;Sum _)
+ (let [flat-sum (type;flatten-variant inputT)]
+ (case (list;nth idx flat-sum)
+ #;None
+ (&;fail (format "Cannot match index " (%n idx) " against type: " (%type inputT)))
+
+ (#;Some case-type)
+ (do Monad<Lux>
+ [[testP nextA] (analyse-pattern #;None case-type (' [(~@ values)]) next)]
+ (wrap [(#lp;Variant [idx (default (list;size flat-sum)
+ num-tags)]
+ testP)
+ nextA]))))
+
+ _
+ (&;fail (pattern-error inputT pattern)))))
+
+ (^ [cursor (#;Form (list& [_ (#;Tag tag)] values))])
+ (&;with-cursor cursor
+ (do Monad<Lux>
+ [tag (macro;normalize tag)
+ [idx group tagT] (macro;resolve-tag tag)
+ _ (&;within-type-env
+ (TC;check inputT tagT))]
+ (analyse-pattern (#;Some (list;size group)) inputT (' ((~ (code;nat idx)) (~@ values))) next)))
+
+ _
+ (&;fail (format "Unrecognized pattern syntax: " (%code pattern)))
+ ))
+
+(def: (analyse-branch analyse inputT pattern body)
+ (-> &;Analyser Type Code Code (Lux [Pattern Analysis]))
+ (analyse-pattern #;None inputT pattern (analyse body)))
+
+(do-template [<name> <tag>]
+ [(def: (<name> coverage)
+ (-> Coverage Bool)
+ (case coverage
+ (<tag> _)
+ true
+
+ _
+ false))]
+
+ [total? #TotalC]
+ [alt? #AltC])
+
+(def: (determine-coverage pattern)
+ (-> Pattern Coverage)
+ (case pattern
+ (^or (#lp;Bind _) #lp;Unit)
+ #TotalC
+
+ (#lp;Bool value)
+ (#BoolC value)
+
+ (^or (#lp;Nat _) (#lp;Int _) (#lp;Deg _)
+ (#lp;Real _) (#lp;Char _) (#lp;Text _))
+ #PartialC
+
+ (#lp;Tuple subs)
+ (loop [subs subs]
+ (case subs
+ #;Nil
+ #TotalC
+
+ (#;Cons sub subs')
+ (let [post (recur subs')]
+ (if (total? post)
+ (determine-coverage sub)
+ (#SeqC (determine-coverage sub)
+ post)))))
+
+ (#lp;Variant [tag-id num-tags] sub)
+ (#VariantC num-tags
+ (|> (D;new number;Hash<Nat>)
+ (D;put tag-id (determine-coverage sub))))))
+
+(def: (xor left right)
+ (-> Bool Bool Bool)
+ (or (and left (not right))
+ (and (not left) right)))
+
+(def: redundant-pattern
+ (R;Result Coverage)
+ (R;fail "Redundant pattern."))
+
+(def: (flatten-alt coverage)
+ (-> Coverage (List Coverage))
+ (case coverage
+ (#AltC left right)
+ (list& left (flatten-alt right))
+
+ _
+ (list coverage)))
+
+(struct: _ (Eq Coverage)
+ (def: (= reference sample)
+ (case [reference sample]
+ (^or [#TotalC #TotalC] [#PartialC #PartialC])
+ true
+
+ [(#BoolC sideR) (#BoolC sideS)]
+ (B/= sideR sideS)
+
+ [(#VariantC allR casesR) (#VariantC allS casesS)]
+ (and (n.= allR allS)
+ (:: (D;Eq<Dict> =) = casesR casesS))
+
+ [(#SeqC leftR rightR) (#SeqC leftS rightS)]
+ (and (= leftR leftS)
+ (= rightR rightS))
+
+ [(#AltC _) (#AltC _)]
+ (let [flatR (flatten-alt reference)
+ flatS (flatten-alt sample)]
+ (and (n.= (list;size flatR) (list;size flatS))
+ (list;every? (function [[coverageR coverageS]]
+ (= coverageR coverageS))
+ (list;zip2 flatR flatS))))
+
+ _
+ false)))
+
+(open Eq<Coverage> "C/")
+
+(def: (merge-coverages addition so-far)
+ (-> Coverage Coverage (R;Result Coverage))
+ (case [addition so-far]
+ ## The addition cannot possibly improve the coverage.
+ [_ #TotalC]
+ redundant-pattern
+
+ ## The addition completes the coverage.
+ [#TotalC _]
+ (R/wrap #TotalC)
+
+ [#PartialC #PartialC]
+ (R/wrap #PartialC)
+
+ (^=> [(#BoolC sideA) (#BoolC sideSF)]
+ (xor sideA sideSF))
+ (R/wrap #TotalC)
+
+ [(#VariantC allA casesA) (#VariantC allSF casesSF)]
+ (cond (not (n.= allSF allA))
+ (R;fail "Variants do not match.")
+
+ (:: (D;Eq<Dict> Eq<Coverage>) = casesSF casesA)
+ redundant-pattern
+
+ ## else
+ (do R;Monad<Result>
+ [casesM (foldM @
+ (function [[tagA coverageA] casesSF']
+ (case (D;get tagA casesSF')
+ (#;Some coverageSF)
+ (do @
+ [coverageM (merge-coverages coverageA coverageSF)]
+ (wrap (D;put tagA coverageM casesSF')))
+
+ #;None
+ (wrap (D;put tagA coverageA casesSF'))))
+ casesSF (D;entries casesA))]
+ (wrap (if (list;every? total? (D;values casesM))
+ #TotalC
+ (#VariantC allSF casesM)))))
+
+ [(#SeqC leftA rightA) (#SeqC leftSF rightSF)]
+ (case [(C/= leftSF leftA) (C/= rightSF rightA)]
+ ## There is nothing the addition adds to the coverage.
+ [true true]
+ redundant-pattern
+
+ ## The 2 sequences cannot possibly be merged.
+ [false false]
+ (R/wrap (#AltC so-far addition))
+
+ ## Same prefix
+ [true false]
+ (do R;Monad<Result>
+ [rightM (merge-coverages rightA rightSF)]
+ (if (total? rightM)
+ (wrap leftSF)
+ (wrap (#SeqC leftSF rightM))))
+
+ ## Same suffix
+ [false true]
+ (do R;Monad<Result>
+ [leftM (merge-coverages leftA leftSF)]
+ (wrap (#SeqC leftM rightA))))
+
+ ## The left part will always match, so the addition is redundant.
+ (^=> [(#SeqC left right) single]
+ (C/= left single))
+ redundant-pattern
+
+ ## The right part is not necessary, since it can always match the left.
+ (^=> [single (#SeqC left right)]
+ (C/= left single))
+ (R/wrap single)
+
+ [_ (#AltC leftS rightS)]
+ (do R;Monad<Result>
+ [#let [fuse-once (: (-> Coverage (List Coverage)
+ (R;Result [(Maybe Coverage)
+ (List Coverage)]))
+ (function [coverage possibilities]
+ (loop [alts possibilities]
+ (case alts
+ #;Nil
+ (wrap [#;None (list coverage)])
+
+ (#;Cons alt alts')
+ (case (merge-coverages coverage alt)
+ (#R;Success altM)
+ (case altM
+ (#AltC _)
+ (do @
+ [[success alts+] (recur alts')]
+ (wrap [success (#;Cons alt alts+)]))
+
+ _
+ (wrap [(#;Some altM) alts']))
+
+ (#R;Error error)
+ (R;fail error))
+ ))))]
+ [success possibilities] (fuse-once addition (flatten-alt so-far))]
+ (loop [success success
+ possibilities possibilities]
+ (case success
+ (#;Some coverage')
+ (do @
+ [[success' possibilities'] (fuse-once coverage' possibilities)]
+ (recur success' possibilities'))
+
+ #;None
+ (case (list;reverse possibilities)
+ #;Nil
+ (R;fail "{ This is not supposed to happen... }")
+
+ (#;Cons last prevs)
+ (wrap (L/fold (function [left right] (#AltC left right))
+ last
+ prevs))))))
+
+ _
+ (if (C/= so-far addition)
+ ## The addition cannot possibly improve the coverage.
+ redundant-pattern
+ ## There are now 2 alternative paths.
+ (R/wrap (#AltC so-far addition)))))
+
+(def: get-coverage
+ (-> [Pattern Analysis] Coverage)
+ (|>. product;left determine-coverage))
+
+(def: #export (analyse-case analyse input branches)
+ (-> &;Analyser Code (List [Code Code]) (Lux Analysis))
+ (case branches
+ #;Nil
+ (&;fail "Cannot have empty branches in pattern-matching expression.")
+
+ (#;Cons [patternH bodyH] branchesT)
+ (do Monad<Lux>
+ [[inputT inputA] (&common;with-unknown-type
+ (analyse input))
+ outputH (analyse-branch analyse inputT patternH bodyH)
+ outputT (mapM @
+ (function [[patternT bodyT]]
+ (analyse-branch analyse inputT patternT bodyT))
+ branchesT)
+ _ (case (foldM R;Monad<Result>
+ merge-coverages
+ (get-coverage outputH)
+ (L/map get-coverage outputT))
+ (#R;Success coverage)
+ (if (total? coverage)
+ (wrap [])
+ (&;fail "Pattern-matching is not total."))
+
+ (#R;Error error)
+ (&;fail error))]
+ (wrap (#la;Case inputA (#;Cons outputH outputT))))))
diff --git a/new-luxc/source/luxc/analyser/function.lux b/new-luxc/source/luxc/analyser/function.lux
index 4b867551e..44deec45b 100644
--- a/new-luxc/source/luxc/analyser/function.lux
+++ b/new-luxc/source/luxc/analyser/function.lux
@@ -50,81 +50,76 @@
(def: #export (analyse-function analyse func-name arg-name body)
(-> &;Analyser Text Text Code (Lux Analysis))
(do Monad<Lux>
- [expected macro;expected-type]
- (&;with-stacked-errors
- (function [_] (format "Functions require function types: " (type;to-text expected)))
- (case expected
- (#;Named name unnamedT)
- (&;with-expected-type unnamedT
- (analyse-function analyse func-name arg-name body))
+ [original macro;expected-type]
+ (loop [expected original]
+ (&;with-stacked-errors
+ (function [_] (format "Functions require function types: " (type;to-text expected)))
+ (case expected
+ (#;Named name unnamedT)
+ (recur unnamedT)
- (#;App funT argT)
- (do @
- [fully-applied (case (type;apply-type funT argT)
- (#;Some value)
- (wrap value)
+ (#;App funT argT)
+ (do @
+ [fully-applied (case (type;apply-type funT argT)
+ (#;Some value)
+ (wrap value)
- #;None
- (&;fail (format "Cannot apply type " (%type funT) " to type " (%type argT))))]
- (&;with-expected-type fully-applied
- (analyse-function analyse func-name arg-name body)))
-
- (#;UnivQ _)
- (do @
- [[var-id var] (&;within-type-env
- TC;existential)]
- (&;with-expected-type (assume (type;apply-type expected var))
- (analyse-function analyse func-name arg-name body)))
+ #;None
+ (&;fail (format "Cannot apply type " (%type funT) " to type " (%type argT))))]
+ (recur fully-applied))
+
+ (#;UnivQ _)
+ (do @
+ [[var-id var] (&;within-type-env
+ TC;existential)]
+ (recur (assume (type;apply-type expected var))))
- (#;ExQ _)
- (&common;with-var
- (function [[var-id var]]
- (&;with-expected-type (assume (type;apply-type expected var))
- (analyse-function analyse func-name arg-name body))))
-
- (#;Var id)
- (do @
- [? (&;within-type-env
- (TC;bound? id))]
- (if ?
- (do @
- [expected' (&;within-type-env
- (TC;read-var id))]
- (&;with-expected-type expected'
- (analyse-function analyse func-name arg-name body)))
- ## Inference
- (&common;with-var
- (function [[input-id inputT]]
- (&common;with-var
- (function [[output-id outputT]]
- (do @
- [#let [funT (#;Function inputT outputT)]
- =function (&;with-expected-type funT
- (analyse-function analyse func-name arg-name body))
- funT' (&;within-type-env
- (TC;clean output-id funT))
- concrete-input? (&;within-type-env
- (TC;bound? input-id))
- funT'' (if concrete-input?
- (&;within-type-env
- (TC;clean input-id funT'))
- (wrap (#;UnivQ (list) (bind-var input-id +1 funT'))))
- _ (&;within-type-env
- (TC;check expected funT''))]
- (wrap =function))
- ))))))
+ (#;ExQ _)
+ (&common;with-var
+ (function [[var-id var]]
+ (recur (assume (type;apply-type expected var)))))
+
+ (#;Var id)
+ (do @
+ [? (&;within-type-env
+ (TC;bound? id))]
+ (if ?
+ (do @
+ [expected' (&;within-type-env
+ (TC;read-var id))]
+ (recur expected'))
+ ## Inference
+ (&common;with-var
+ (function [[input-id inputT]]
+ (&common;with-var
+ (function [[output-id outputT]]
+ (do @
+ [#let [funT (#;Function inputT outputT)]
+ =function (recur funT)
+ funT' (&;within-type-env
+ (TC;clean output-id funT))
+ concrete-input? (&;within-type-env
+ (TC;bound? input-id))
+ funT'' (if concrete-input?
+ (&;within-type-env
+ (TC;clean input-id funT'))
+ (wrap (#;UnivQ (list) (bind-var input-id +1 funT'))))
+ _ (&;within-type-env
+ (TC;check expected funT''))]
+ (wrap =function))
+ ))))))
- (#;Function inputT outputT)
- (<| (:: @ map (|>. #la;Function))
- &;with-scope
- (&env;with-local [func-name expected])
- (&env;with-local [arg-name inputT])
- (&;with-expected-type outputT)
- (analyse body))
-
- _
- (&;fail "")
- ))))
+ (#;Function inputT outputT)
+ (<| (:: @ map (|>. #la;Function))
+ &;with-scope
+ (&env;with-local [func-name original])
+ (&env;with-local [arg-name inputT])
+ (&;with-expected-type outputT)
+ (analyse body))
+
+ _
+ (&;fail "")
+ )))))
(def: (analyse-apply' analyse funcT args)
(-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
diff --git a/new-luxc/source/luxc/analyser/pattern.lux b/new-luxc/source/luxc/analyser/pattern.lux
deleted file mode 100644
index f4a14d855..000000000
--- a/new-luxc/source/luxc/analyser/pattern.lux
+++ /dev/null
@@ -1,3 +0,0 @@
-(;module:
- lux)
-
diff --git a/new-luxc/source/luxc/analyser/struct.lux b/new-luxc/source/luxc/analyser/struct.lux
index 0ca3c9f63..1fbca886f 100644
--- a/new-luxc/source/luxc/analyser/struct.lux
+++ b/new-luxc/source/luxc/analyser/struct.lux
@@ -6,11 +6,14 @@
(concurrency ["A" atom])
(data [text "T/" Eq<Text>]
text/format
+ [ident]
(coll [list "L/" Fold<List> Monoid<List> Monad<List>]
- ["D" dict])
+ ["D" dict]
+ ["S" set])
[number]
[product])
[macro #+ Monad<Lux>]
+ (macro [code])
[type]
(type ["TC" check]))
(luxc ["&" base]
@@ -169,3 +172,65 @@
_
(&;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])))