From 0abd5bd3c0e38e352e9ba38268e04e1c858ab01e Mon Sep 17 00:00:00 2001 From: Eduardo Julian Date: Thu, 15 Jul 2021 00:45:15 -0400 Subject: Re-named "spec" hierarchy to "specification". --- .../compositor/generation/structure.lux | 89 ++++++++++++++++++++++ 1 file changed, 89 insertions(+) create mode 100644 stdlib/source/specification/compositor/generation/structure.lux (limited to 'stdlib/source/specification/compositor/generation/structure.lux') diff --git a/stdlib/source/specification/compositor/generation/structure.lux b/stdlib/source/specification/compositor/generation/structure.lux new file mode 100644 index 000000000..7c45d2a9b --- /dev/null +++ b/stdlib/source/specification/compositor/generation/structure.lux @@ -0,0 +1,89 @@ +(.module: + [lux #* + ["_" test (#+ Test)] + [abstract + [monad (#+ do)]] + [control + [pipe (#+ case>)] + ["." try]] + [data + ["." maybe] + [number + ["n" nat] + ["i" int]] + ["." text ("#\." equivalence) + ["%" format (#+ format)]] + [collection + ["." array (#+ Array)] + ["." list ("#\." functor)]]] + [math + ["r" random]] + ["." ffi (#+ import:)] + [tool + [compiler + ["." analysis] + ["." synthesis]]]] + [/// + [common (#+ Runner)]]) + +(import: java/lang/Integer) + +(def: (variant run) + (-> Runner Test) + (do {! r.monad} + [num-tags (|> r.nat (\ ! map (|>> (n.% 10) (n.max 2)))) + tag-in (|> r.nat (\ ! map (n.% num-tags))) + #let [last?-in (|> num-tags dec (n.= tag-in))] + value-in r.i64] + (_.test (%.name (name-of synthesis.variant)) + (|> (synthesis.variant {#analysis.lefts (if last?-in + (dec tag-in) + tag-in) + #analysis.right? last?-in + #analysis.value (synthesis.i64 value-in)}) + (run "variant") + (case> (#try.Success valueT) + (let [valueT (:as (Array Any) valueT)] + (and (n.= 3 (array.size valueT)) + (let [tag-out (:as java/lang/Integer (maybe.assume (array.read 0 valueT))) + last?-out (array.read 1 valueT) + value-out (:as Any (maybe.assume (array.read 2 valueT))) + same-tag? (|> tag-out ffi.int-to-long (:as Nat) (n.= tag-in)) + same-flag? (case last?-out + (#.Some last?-out') + (and last?-in (text\= "" (:as Text last?-out'))) + + #.None + (not last?-in)) + same-value? (|> value-out (:as Int) (i.= value-in))] + (and same-tag? + same-flag? + same-value?)))) + + (#try.Failure _) + false))))) + +(def: (tuple run) + (-> Runner Test) + (do {! r.monad} + [size (|> r.nat (\ ! map (|>> (n.% 10) (n.max 2)))) + tuple-in (r.list size r.i64)] + (_.test (%.name (name-of synthesis.tuple)) + (|> (synthesis.tuple (list\map (|>> synthesis.i64) tuple-in)) + (run "tuple") + (case> (#try.Success tuple-out) + (let [tuple-out (:as (Array Any) tuple-out)] + (and (n.= size (array.size tuple-out)) + (list.every? (function (_ [left right]) + (i.= left (:as Int right))) + (list.zip/2 tuple-in (array.to-list tuple-out))))) + + (#try.Failure _) + false))))) + +(def: #export (spec runner) + (-> Runner Test) + ($_ _.and + (..variant runner) + (..tuple runner) + )) -- cgit v1.2.3