move examples to root
This commit is contained in:
parent
c9fd66160b
commit
6f469cdad7
2 changed files with 2 additions and 2 deletions
68
examples/maybe.nix
Normal file
68
examples/maybe.nix
Normal file
|
|
@ -0,0 +1,68 @@
|
|||
{nt, ...}: let
|
||||
inherit
|
||||
(nt.util)
|
||||
ntTrapdoorKey
|
||||
ntDynamicTrapdoorKey
|
||||
mkTrapdoorFn
|
||||
mkTrapdoorSet
|
||||
;
|
||||
in {
|
||||
# NOTE: Maybe is used to simplify parsing Type/Class declarations
|
||||
# NOTE: and therefore must be implemented manually
|
||||
Maybe = let
|
||||
meta = instance: {
|
||||
sig = "nt::&Maybe";
|
||||
derive = [];
|
||||
ops = {};
|
||||
req = {"nt::&Maybe" = ["unwrap"];};
|
||||
};
|
||||
in
|
||||
mkTrapdoorFn {
|
||||
default = {
|
||||
unwrap = "TODO";
|
||||
};
|
||||
unlock.${ntTrapdoorKey} = meta false;
|
||||
};
|
||||
|
||||
Some = let
|
||||
meta = instance: {
|
||||
inherit instance;
|
||||
sig = "nt::Some";
|
||||
derive = ["nt::&Maybe"];
|
||||
ops = {
|
||||
"nt::&Maybe".unwrap = f: self: f self.${ntDynamicTrapdoorKey}.value;
|
||||
};
|
||||
req = {};
|
||||
};
|
||||
in
|
||||
mkTrapdoorFn {
|
||||
default = value:
|
||||
mkTrapdoorSet {
|
||||
unlock = {
|
||||
${ntTrapdoorKey} = meta true;
|
||||
${ntDynamicTrapdoorKey} = {
|
||||
inherit value;
|
||||
};
|
||||
};
|
||||
};
|
||||
unlock.${ntTrapdoorKey} = meta false;
|
||||
};
|
||||
|
||||
None = let
|
||||
meta = instance: {
|
||||
inherit instance;
|
||||
sig = "nt::None";
|
||||
derive = ["nt::&Maybe"];
|
||||
ops = {
|
||||
"nt::&Maybe".map = f: self: self;
|
||||
};
|
||||
req = {};
|
||||
};
|
||||
in
|
||||
mkTrapdoorFn {
|
||||
default = mkTrapdoorSet ntTrapdoorKey {
|
||||
unlock = meta true;
|
||||
};
|
||||
unlock.${ntTrapdoorKey} = meta false;
|
||||
};
|
||||
}
|
||||
75
examples/rose.nix
Normal file
75
examples/rose.nix
Normal file
|
|
@ -0,0 +1,75 @@
|
|||
{
|
||||
nib,
|
||||
# typespace,
|
||||
...
|
||||
}: let
|
||||
inherit
|
||||
(nib)
|
||||
Attrs
|
||||
Bool
|
||||
contains
|
||||
expect
|
||||
flipCurry
|
||||
Fn
|
||||
getHidden
|
||||
Meta
|
||||
PartialOrder
|
||||
Prod
|
||||
Sum
|
||||
Type
|
||||
Class
|
||||
UnFn # UnFn = Fn Any Any
|
||||
;
|
||||
in {
|
||||
# Rose = Struct "nib::Rose" (Rose: {
|
||||
Rose = Type "nib::Rose" (Self: {
|
||||
ops = {
|
||||
# elements can either be an attribute set, or a function/lambda
|
||||
# roses :: [Rose]
|
||||
Type.mk = meta: roses: {
|
||||
expose = roses;
|
||||
hidden = {inherit meta;};
|
||||
};
|
||||
|
||||
PartialOrder.leq = flipCurry contains;
|
||||
|
||||
Meta.get = R: (getHidden R).meta;
|
||||
};
|
||||
|
||||
derive = [
|
||||
PartialOrder
|
||||
Meta
|
||||
];
|
||||
});
|
||||
|
||||
PartialOrder = Class "nib::&PartialOrder" (Self: {
|
||||
ops = {
|
||||
# NOTE: `Prod A B` == `Prod [A B]`
|
||||
leq = expect <| Fn (Prod Self Self) Bool;
|
||||
gt = ! Self.leq;
|
||||
};
|
||||
});
|
||||
|
||||
Meta = Class "nib::&Meta" {
|
||||
# NOTE: `Sum A B` == `Sum [A B]`
|
||||
attrs.hidden.meta = expect <| Sum [UnFn Attrs];
|
||||
ops.get = T: (getHidden T).meta;
|
||||
};
|
||||
|
||||
ProperType = Class "nib::&ProperType" (Self: {
|
||||
ops.mk = expect <| Sum [UnFn Self];
|
||||
});
|
||||
|
||||
Trivial =
|
||||
Class "nib::&Trivial" {
|
||||
};
|
||||
|
||||
# We can now do the following:
|
||||
# `Rose.mk meta [...]` <-> `Rose meta [...]`
|
||||
# Rose.leq roseA roseB
|
||||
# Rose.meta roseA
|
||||
# Rose.verify # Verify all Axioms
|
||||
|
||||
# in Cerulean: (Nix-style type extensions via overlays/overrides)
|
||||
# Group = nib.overrideStruct Rose (prev: { ... });
|
||||
}
|
||||
Loading…
Add table
Add a link
Reference in a new issue