From 8ba6ac8952e3457b1a09e30ac5312168d48006d1 Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Wed, 16 May 2018 00:11:49 -0400 Subject: - Migrated structure analysis to stdlib. - Added an easy way to report information in exceptions. --- new-luxc/test/test/luxc/lang/analysis/common.lux | 22 -- .../test/test/luxc/lang/analysis/structure.lux | 331 --------------------- 2 files changed, 353 deletions(-) delete mode 100644 new-luxc/test/test/luxc/lang/analysis/structure.lux (limited to 'new-luxc/test') diff --git a/new-luxc/test/test/luxc/lang/analysis/common.lux b/new-luxc/test/test/luxc/lang/analysis/common.lux index 35212e55d..7e343cc88 100644 --- a/new-luxc/test/test/luxc/lang/analysis/common.lux +++ b/new-luxc/test/test/luxc/lang/analysis/common.lux @@ -11,28 +11,6 @@ [eval])) (test/luxc common)) -(def: gen-unit - (r.Random Code) - (r/wrap (' []))) - -(def: #export gen-primitive - (r.Random [Type Code]) - (with-expansions - [ (do-template [ ] - [(r.seq (r/wrap ) (r/map ))] - - [Top code.tuple (r.list +0 gen-unit)] - [Bool code.bool r.bool] - [Nat code.nat r.nat] - [Int code.int r.int] - [Deg code.deg r.deg] - [Frac code.frac r.frac] - [Text code.text (r.text +5)] - )] - ($_ r.either - - ))) - (def: #export analyse &.Analyser (expressionA.analyser eval.eval)) diff --git a/new-luxc/test/test/luxc/lang/analysis/structure.lux b/new-luxc/test/test/luxc/lang/analysis/structure.lux deleted file mode 100644 index 0a94e37da..000000000 --- a/new-luxc/test/test/luxc/lang/analysis/structure.lux +++ /dev/null @@ -1,331 +0,0 @@ -(.module: - lux - (lux [io] - (control [monad #+ do] - pipe) - (data [bool "bool/" Eq] - ["e" error] - [product] - [maybe] - [text] - text/format - (coll [list "list/" Functor] - (set ["set" unordered]))) - ["r" math/random "r/" Monad] - [macro] - (macro [code]) - (lang [type "type/" Eq] - (type ["tc" check])) - test) - (luxc ["&" lang] - (lang ["@." module] - ["la" analysis] - (analysis [".A" expression] - ["@" structure] - ["@." common]))) - (// common) - (test/luxc common)) - -(context: "Sums" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2)))) - choice (|> r.nat (:: @ map (n/% size))) - primitives (r.list size gen-primitive) - +choice (|> r.nat (:: @ map (n/% (n/inc size)))) - [_ +valueC] gen-primitive - #let [variantT (type.variant (list/map product.left primitives)) - [valueT valueC] (maybe.assume (list.nth choice primitives)) - +size (n/inc size) - +primitives (list.concat (list (list.take choice primitives) - (list [(#.Bound +1) +valueC]) - (list.drop choice primitives))) - [+valueT +valueC] (maybe.assume (list.nth +choice +primitives)) - +variantT (type.variant (list/map product.left +primitives))]] - ($_ seq - (test "Can analyse sum." - (|> (&.with-scope - (&.with-type variantT - (@.analyse-sum analyse choice valueC))) - (macro.run (io.run init-jvm)) - (case> (^multi (#e.Success [_ sumA]) - [(la.unfold-variant sumA) - (#.Some [tag last? valueA])]) - (and (n/= tag choice) - (bool/= last? (n/= (n/dec size) choice))) - - _ - false))) - (test "Can analyse sum through bound type-vars." - (|> (&.with-scope - (do macro.Monad - [[_ varT] (&.with-type-env tc.var) - _ (&.with-type-env - (tc.check varT variantT))] - (&.with-type varT - (@.analyse-sum analyse choice valueC)))) - (macro.run (io.run init-jvm)) - (case> (^multi (#e.Success [_ sumA]) - [(la.unfold-variant sumA) - (#.Some [tag last? valueA])]) - (and (n/= tag choice) - (bool/= last? (n/= (n/dec size) choice))) - - _ - false))) - (test "Cannot analyse sum through unbound type-vars." - (|> (&.with-scope - (do macro.Monad - [[_ varT] (&.with-type-env tc.var)] - (&.with-type varT - (@.analyse-sum analyse choice valueC)))) - (macro.run (io.run init-jvm)) - (case> (#e.Success _) - false - - _ - true))) - (test "Can analyse sum through existential quantification." - (|> (&.with-scope - (&.with-type (type.ex-q +1 +variantT) - (@.analyse-sum analyse +choice +valueC))) - (macro.run (io.run init-jvm)) - (case> (#e.Success _) - true - - (#e.Error error) - false))) - (test "Can analyse sum through universal quantification." - (|> (&.with-scope - (&.with-type (type.univ-q +1 +variantT) - (@.analyse-sum analyse +choice +valueC))) - (macro.run (io.run init-jvm)) - (case> (#e.Success _) - (not (n/= choice +choice)) - - (#e.Error error) - (n/= choice +choice)))) - )))) - -(context: "Products" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2)))) - primitives (r.list size gen-primitive) - choice (|> r.nat (:: @ map (n/% size))) - [_ +valueC] gen-primitive - #let [[singletonT singletonC] (|> primitives (list.nth choice) maybe.assume) - +primitives (list.concat (list (list.take choice primitives) - (list [(#.Bound +1) +valueC]) - (list.drop choice primitives))) - +tupleT (type.tuple (list/map product.left +primitives))]] - ($_ seq - (test "Can analyse product." - (|> (&.with-type (type.tuple (list/map product.left primitives)) - (@.analyse-product analyse (list/map product.right primitives))) - (macro.run (io.run init-jvm)) - (case> (#e.Success tupleA) - (n/= size (list.size (la.unfold-tuple tupleA))) - - _ - false))) - (test "Can infer product." - (|> (@common.with-unknown-type - (@.analyse-product analyse (list/map product.right primitives))) - (macro.run (io.run init-jvm)) - (case> (#e.Success [_type tupleA]) - (and (type/= (type.tuple (list/map product.left primitives)) - _type) - (n/= size (list.size (la.unfold-tuple tupleA)))) - - _ - false))) - (test "Can analyse pseudo-product (singleton tuple)" - (|> (&.with-type singletonT - (analyse (` [(~ singletonC)]))) - (macro.run (io.run init-jvm)) - (case> (#e.Success singletonA) - true - - (#e.Error error) - false))) - (test "Can analyse product through bound type-vars." - (|> (&.with-scope - (do macro.Monad - [[_ varT] (&.with-type-env tc.var) - _ (&.with-type-env - (tc.check varT (type.tuple (list/map product.left primitives))))] - (&.with-type varT - (@.analyse-product analyse (list/map product.right primitives))))) - (macro.run (io.run init-jvm)) - (case> (#e.Success [_ tupleA]) - (n/= size (list.size (la.unfold-tuple tupleA))) - - _ - false))) - (test "Can analyse product through existential quantification." - (|> (&.with-scope - (&.with-type (type.ex-q +1 +tupleT) - (@.analyse-product analyse (list/map product.right +primitives)))) - (macro.run (io.run init-jvm)) - (case> (#e.Success _) - true - - (#e.Error error) - false))) - (test "Cannot analyse product through universal quantification." - (|> (&.with-scope - (&.with-type (type.univ-q +1 +tupleT) - (@.analyse-product analyse (list/map product.right +primitives)))) - (macro.run (io.run init-jvm)) - (case> (#e.Success _) - false - - (#e.Error error) - true))) - )))) - -(def: (check-variant variantT choice size analysis) - (-> Type Nat Nat (Meta [Module Scope la.Analysis]) Bool) - (|> analysis - (&.with-type variantT) - (macro.run (io.run init-jvm)) - (case> (^multi (#e.Success [_ _ sumA]) - [(la.unfold-variant sumA) - (#.Some [tag last? valueA])]) - (and (n/= tag choice) - (bool/= last? (n/= (n/dec size) choice))) - - _ - false))) - -(def: (check-record-inference tupleT size analysis) - (-> Type Nat (Meta [Module Scope Type la.Analysis]) Bool) - (|> analysis - (macro.run (io.run init-jvm)) - (case> (^multi (#e.Success [_ _ productT productA]) - [(la.unfold-tuple productA) - membersA]) - (and (type/= tupleT productT) - (n/= size (list.size membersA))) - - _ - false))) - -(context: "Tagged Sums" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2)))) - tags (|> (r.set text.Hash size (r.text +5)) (:: @ map set.to-list)) - choice (|> r.nat (:: @ map (n/% size))) - other-choice (|> r.nat (:: @ map (n/% size)) (r.filter (|>> (n/= choice) not))) - primitives (r.list size gen-primitive) - module-name (r.text +5) - type-name (r.text +5) - #let [varT (#.Bound +1) - primitivesT (list/map product.left primitives) - [choiceT choiceC] (maybe.assume (list.nth choice primitives)) - [other-choiceT other-choiceC] (maybe.assume (list.nth other-choice primitives)) - variantT (type.variant primitivesT) - namedT (#.Named [module-name type-name] variantT) - polyT (|> (type.variant (list.concat (list (list.take choice primitivesT) - (list varT) - (list.drop (n/inc choice) primitivesT)))) - (type.univ-q +1)) - named-polyT (#.Named [module-name type-name] polyT) - choice-tag (maybe.assume (list.nth choice tags)) - other-choice-tag (maybe.assume (list.nth other-choice tags))]] - ($_ seq - (test "Can infer tagged sum." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false namedT)] - (&.with-scope - (@.analyse-tagged-sum analyse [module-name choice-tag] choiceC)))) - (check-variant variantT choice size))) - (test "Tagged sums specialize when type-vars get bound." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false named-polyT)] - (&.with-scope - (@.analyse-tagged-sum analyse [module-name choice-tag] choiceC)))) - (check-variant variantT choice size))) - (test "Tagged sum inference retains universal quantification when type-vars are not bound." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false named-polyT)] - (&.with-scope - (@.analyse-tagged-sum analyse [module-name other-choice-tag] other-choiceC)))) - (check-variant polyT other-choice size))) - (test "Can specialize generic tagged sums." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false named-polyT)] - (&.with-scope - (&.with-type variantT - (@.analyse-tagged-sum analyse [module-name other-choice-tag] other-choiceC))))) - (macro.run (io.run init-jvm)) - (case> (^multi (#e.Success [_ _ sumA]) - [(la.unfold-variant sumA) - (#.Some [tag last? valueA])]) - (and (n/= tag other-choice) - (bool/= last? (n/= (n/dec size) other-choice))) - - _ - false))) - )))) - -(context: "Records" - (<| (times +100) - (do @ - [size (|> r.nat (:: @ map (|>> (n/% +10) (n/max +2)))) - tags (|> (r.set text.Hash size (r.text +5)) (:: @ map set.to-list)) - primitives (r.list size gen-primitive) - module-name (r.text +5) - type-name (r.text +5) - choice (|> r.nat (:: @ map (n/% size))) - #let [varT (#.Bound +1) - tagsC (list/map (|>> [module-name] code.tag) tags) - primitivesT (list/map product.left primitives) - primitivesC (list/map product.right primitives) - tupleT (type.tuple primitivesT) - namedT (#.Named [module-name type-name] tupleT) - recordC (list.zip2 tagsC primitivesC) - polyT (|> (type.tuple (list.concat (list (list.take choice primitivesT) - (list varT) - (list.drop (n/inc choice) primitivesT)))) - (type.univ-q +1)) - named-polyT (#.Named [module-name type-name] polyT)]] - ($_ seq - (test "Can infer record." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false namedT)] - (&.with-scope - (@common.with-unknown-type - (@.analyse-record analyse recordC))))) - (check-record-inference tupleT size))) - (test "Records specialize when type-vars get bound." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false named-polyT)] - (&.with-scope - (@common.with-unknown-type - (@.analyse-record analyse recordC))))) - (check-record-inference tupleT size))) - (test "Can specialize generic records." - (|> (@module.with-module +0 module-name - (do macro.Monad - [_ (@module.declare-tags tags false named-polyT)] - (&.with-scope - (&.with-type tupleT - (@.analyse-record analyse recordC))))) - (macro.run (io.run init-jvm)) - (case> (^multi (#e.Success [_ _ productA]) - [(la.unfold-tuple productA) - membersA]) - (n/= size (list.size membersA)) - - _ - false))) - )))) -- cgit v1.2.3