Port fixed-point.nix

This commit is contained in:
Charlotte 🦝 Delenk 2022-09-09 08:23:27 +01:00
parent f3b636b485
commit 850b53a4a1
Signed by: darkkirb
GPG key ID: AB2BD8DAF2E37122
7 changed files with 171 additions and 1 deletions

View file

@ -0,0 +1,18 @@
λ(nix : ../NixPrelude.dhall) →
let Set = ../Set/Type.dhall
let Set/mergeAttrs = ../Set/mergeAttrs.dhall nix
let composeExtensions
: (Set → Set → Set) → (Set → Set → Set) → Set → Set → Set
= λ(f : Set → Set → Set) →
λ(g : Set → Set → Set) →
λ(final : Set) →
λ(prev : Set) →
let fApplied = f final prev
let prevp = Set/mergeAttrs prev fApplied
in Set/mergeAttrs fApplied (g final prevp)
in composeExtensions

View file

@ -0,0 +1,24 @@
λ(nix : ../NixPrelude.dhall) →
let Any = ../Any/Type.dhall
let Set = ../Set/Type.dhall
let composeExtensions = ./composeExtensions.dhall nix
let Set/toSet = ../Set/toSet.dhall nix
let Map =
https://prelude.dhall-lang.org/Map/Type.dhall
sha256:210c7a9eba71efbb0f7a66b3dcf8b9d3976ffc2bc0e907aadfb6aa29c333e8ed
let composeManyExtensions
: List (Set → Set → Set) → Set → Set → Set
= λ(list : List (Set → Set → Set)) →
List/fold
(Set → Set → Set)
list
(Set → Set → Set)
composeExtensions
(λ(final : Set) → λ(prev : Set) → Set/toSet Any ([] : Map Text Any))
in composeManyExtensions

34
Function/converge.dhall Normal file
View file

@ -0,0 +1,34 @@
λ(nix : ../NixPrelude.dhall) →
let Any = ../Any/Type.dhall
let Any/toAny = ../Any/toAny.dhall nix
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
let Any/equal = ../Any/equal.dhall nix
in λ(t : Type) →
let FunctionType = λ(x : Type) → x → (t → t) → t → t
let function =
λ(function : FunctionType Any) →
let functionArgs =
Any/toTypeUnchecked
(FunctionType (FunctionType Any))
(Any/toAny (FunctionType Any) function)
function
in λ(f : t → t) →
λ(x : t) →
let xp = f x
in if Any/equal (Any/toAny t xp) (Any/toAny t x)
then x
else functionArgs f xp
let functionErased =
Any/toTypeUnchecked
(FunctionType Any)
(Any/toAny (FunctionType (FunctionType Any)) function)
in function functionErased

13
Function/extends.dhall Normal file
View file

@ -0,0 +1,13 @@
λ(nix : ../NixPrelude.dhall) →
let Set = ../Set/Type.dhall
let Set/mergeAttrs = ../Set/mergeAttrs.dhall nix
let extends
: (Set → Set → Set) → (Set → Set) → Set → Set
= λ(f : Set → Set → Set) →
λ(rattrs : Set → Set) →
λ(self : Set) →
let super = rattrs self in Set/mergeAttrs super (f super self)
in extends

22
Function/fix.dhall Normal file
View file

@ -0,0 +1,22 @@
λ(nix : ../NixPrelude.dhall) →
let fixSrc = "f: let x = f x; in x"
let fixSrcp = "f: let x = f x // { __unfix__ = f; }; in x"
let fixFile = nix.builtins.toFile "fix.nix" fixSrc
let fixFilep = nix.builtins.toFile "fix.nix" fixSrcp
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
let fix
: ∀(t : Type) → (t → t) → t
= λ(t : Type) →
Any/toTypeUnchecked ((t → t) → t) (nix.builtins.import fixFile)
let fixp
: ∀(t : Type) → (t → t) → t
= λ(t : Type) →
Any/toTypeUnchecked ((t → t) → t) (nix.builtins.import fixFilep)
in { fix, fixp }

View file

@ -0,0 +1,51 @@
λ(nix : ../NixPrelude.dhall) →
let Any = ../Any/Type.dhall
let Set = ../Set/Type.dhall
let Any/toAny = ../Any/toAny.dhall nix
let Any/toTypeUnchecked = ../Any/toTypeUnchecked.dhall nix
let fixp = (./fix.dhall nix).fixp Set
let Set/toSet = ../Set/toSet.dhall nix
let Set/mergeAttrs = ../Set/mergeAttrs.dhall nix
let extends = ./extends.dhall nix
let FunctionType = λ(x : Type) → x → Text → (Set → Set) → Set
let function =
λ(function : FunctionType Any) →
let functionArgs =
Any/toTypeUnchecked
(FunctionType (FunctionType Any))
(Any/toAny (FunctionType Any) function)
function
in λ(extenderName : Text) →
λ(rattrs : Set → Set) →
let extset =
Set/toSet
((Set → Set → Set) → Set)
[ { mapKey = extenderName
, mapValue =
λ(f : Set → Set → Set) →
functionArgs extenderName (extends f rattrs)
}
]
in Set/mergeAttrs (fixp rattrs) extset
let functionErased =
Any/toTypeUnchecked
(FunctionType Any)
(Any/toAny (FunctionType (FunctionType Any)) function)
let makeExtensibleWithCustomName
: Text → (Set → Set) → Set
= function functionErased
in makeExtensibleWithCustomName

View file

@ -1,8 +1,16 @@
λ(nix : ../NixPrelude.dhall) → λ(nix : ../NixPrelude.dhall) →
{ const = ./const.dhall { composeExtensions = ./composeExtensions.dhall nix
, composeManyExtensions = ./composeManyExtensions.dhall nix
, const = ./const.dhall
, converge = ./converge.dhall nix
, deepSeq = ./seq.dhall nix , deepSeq = ./seq.dhall nix
, extends = ./extends.dhall nix
, fix = (./fix.dhall nix).fix
, fixp = (./fix.dhall nix).fixp
, flip = ./flip.dhall , flip = ./flip.dhall
, functionArgs = ./functionArgs.dhall nix , functionArgs = ./functionArgs.dhall nix
, makeExtensible = ./makeExtensibleWithCustomName.dhall nix "extend"
, makeExtensibleWithCustomName = ./makeExtensibleWithCustomName.dhall nix
, pipe = ./pipe.dhall , pipe = ./pipe.dhall
, setFunctionArgs = ./setFunctionArgs.dhall nix , setFunctionArgs = ./setFunctionArgs.dhall nix
, seq = ./seq.dhall nix , seq = ./seq.dhall nix