aboutsummaryrefslogtreecommitdiff
path: root/new-luxc/test
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--new-luxc/test/test/luxc/lang/analysis/function.lux141
1 files changed, 0 insertions, 141 deletions
diff --git a/new-luxc/test/test/luxc/lang/analysis/function.lux b/new-luxc/test/test/luxc/lang/analysis/function.lux
deleted file mode 100644
index 968de53ef..000000000
--- a/new-luxc/test/test/luxc/lang/analysis/function.lux
+++ /dev/null
@@ -1,141 +0,0 @@
-(.module:
- lux
- (lux [io]
- (control [monad #+ do]
- pipe)
- (data ["e" error]
- [maybe]
- [product]
- [text "text/" Eq<Text>]
- text/format
- (coll [list "list/" Functor<List>]))
- ["r" math/random "r/" Monad<Random>]
- [macro]
- (macro [code])
- (lang [type "type/" Eq<Type>])
- test)
- (luxc ["&" lang]
- (lang ["@." module]
- ["la" analysis]
- (analysis [".A" expression]
- ["@" function]
- ["@." common])))
- (// common)
- (test/luxc common))
-
-(def: (check-type expectedT error)
- (-> Type (e.Error [Type la.Analysis]) Bool)
- (case error
- (#e.Success [exprT exprA])
- (type/= expectedT exprT)
-
- _
- false))
-
-(def: (succeeds? error)
- (All [a] (-> (e.Error a) Bool))
- (case error
- (#e.Success _)
- true
-
- (#e.Error _)
- false))
-
-(def: (flatten-apply analysis)
- (-> la.Analysis [la.Analysis (List la.Analysis)])
- (case analysis
- (^code ("lux apply" (~ head) (~ func)))
- (let [[func' tail] (flatten-apply func)]
- [func' (#.Cons head tail)])
-
- _
- [analysis (list)]))
-
-(def: (check-apply expectedT num-args analysis)
- (-> Type Nat (Meta la.Analysis) Bool)
- (|> analysis
- (&.with-type expectedT)
- (macro.run (io.run init-jvm))
- (case> (#e.Success applyA)
- (let [[funcA argsA] (flatten-apply applyA)]
- (n/= num-args (list.size argsA)))
-
- (#e.Error error)
- false)))
-
-(context: "Function definition."
- (<| (times +100)
- (do @
- [func-name (r.text +5)
- arg-name (|> (r.text +5) (r.filter (|>> (text/= func-name) not)))
- [outputT outputC] gen-primitive
- [inputT _] gen-primitive
- #let [g!arg (code.local-symbol arg-name)]]
- ($_ seq
- (test "Can analyse function."
- (and (|> (&.with-type (All [a] (-> a outputT))
- (@.analyse-function analyse func-name arg-name outputC))
- (macro.run (io.run init-jvm))
- succeeds?)
- (|> (&.with-type (All [a] (-> a a))
- (@.analyse-function analyse func-name arg-name g!arg))
- (macro.run (io.run init-jvm))
- succeeds?)))
- (test "Generic functions can always be specialized."
- (and (|> (&.with-type (-> inputT outputT)
- (@.analyse-function analyse func-name arg-name outputC))
- (macro.run (io.run init-jvm))
- succeeds?)
- (|> (&.with-type (-> inputT inputT)
- (@.analyse-function analyse func-name arg-name g!arg))
- (macro.run (io.run init-jvm))
- succeeds?)))
- (test "The function's name is bound to the function's type."
- (|> (&.with-type (Rec self (-> inputT self))
- (@.analyse-function analyse func-name arg-name (code.local-symbol func-name)))
- (macro.run (io.run init-jvm))
- succeeds?))
- ))))
-
-(context: "Function application."
- (<| (times +100)
- (do @
- [full-args (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2))))
- partial-args (|> r.nat (:: @ map (n/% full-args)))
- var-idx (|> r.nat (:: @ map (|>> (n/% full-args) (n/max +1))))
- inputsTC (r.list full-args gen-primitive)
- #let [inputsT (list/map product.left inputsTC)
- inputsC (list/map product.right inputsTC)]
- [outputT outputC] gen-primitive
- #let [funcT (type.function inputsT outputT)
- partialT (type.function (list.drop partial-args inputsT) outputT)
- varT (#.Bound +1)
- polyT (<| (type.univ-q +1)
- (type.function (list.concat (list (list.take var-idx inputsT)
- (list varT)
- (list.drop (n/inc var-idx) inputsT))))
- varT)
- poly-inputT (maybe.assume (list.nth var-idx inputsT))
- partial-poly-inputsT (list.drop (n/inc var-idx) inputsT)
- partial-polyT1 (<| (type.function partial-poly-inputsT)
- poly-inputT)
- partial-polyT2 (<| (type.univ-q +1)
- (type.function (#.Cons varT partial-poly-inputsT))
- varT)]]
- ($_ seq
- (test "Can analyse monomorphic type application."
- (|> (@.analyse-apply analyse funcT (' []) inputsC)
- (check-apply outputT full-args)))
- (test "Can partially apply functions."
- (|> (@.analyse-apply analyse funcT (' []) (list.take partial-args inputsC))
- (check-apply partialT partial-args)))
- (test "Can apply polymorphic functions."
- (|> (@.analyse-apply analyse polyT (' []) inputsC)
- (check-apply poly-inputT full-args)))
- (test "Polymorphic partial application propagates found type-vars."
- (|> (@.analyse-apply analyse polyT (' []) (list.take (n/inc var-idx) inputsC))
- (check-apply partial-polyT1 (n/inc var-idx))))
- (test "Polymorphic partial application preserves quantification for type-vars."
- (|> (@.analyse-apply analyse polyT (' []) (list.take var-idx inputsC))
- (check-apply partial-polyT2 var-idx)))
- ))))