diff --git a/test_workspace/BuildLibrary.bosatsu b/test_workspace/BuildLibrary.bosatsu index cf9c12604..f1f99759f 100644 --- a/test_workspace/BuildLibrary.bosatsu +++ b/test_workspace/BuildLibrary.bosatsu @@ -5,25 +5,21 @@ export File(), Library(), LibArgs(), build, Build, file, files, build_all, libra struct Leibniz[a, b](cast: forall f: * -> *. f[a] -> f[b]) (refl: forall a. Leibniz[a, a]) = Leibniz(x -> x) -# In Bosatsu, like System F, the type exists a. P can be encoded as forall b. (forall a. P -> b) -> b -# We encode Mapped in this way, we want: Mapped(to_tuple: exists b. (Build[b], b -> a)) -# we write: Mapped(to_tuple: forall c. (forall b. (Build[b], b -> a) -> c) -> c) - struct File(path: String) struct Library enum Build[a]: LoadFile(name: String, is_file: Leibniz[a, File]) Pure(value: a) - Mapped(consume: forall b. (forall c. (Build[c], c -> a) -> b) -> b) - Map2(consume: forall b. (forall c, d. (Build[c], Build[d], (c, d) -> a) -> b) -> b) + Mapped(consume: exists b. (Build[b], b -> a)) + Map2(consume: exists b, c. (Build[b], Build[c], (b, c) -> a)) BuildLib(files: Build[List[File]], deps: Build[List[Library]], is_lib: Leibniz[a, Library]) def map_Build(b: Build[a], fn: a -> b) -> Build[b]: - Mapped(cb -> cb(b, fn)) + Mapped((b, fn)) def map2_Build(ba: Build[a], bb: Build[b], fn: (a, b) -> c) -> Build[c]: - Map2(cb -> cb(ba, bb, fn)) + Map2((ba, bb, fn)) def file(s: String) -> Build[File]: LoadFile(s, refl)