/usr/share/axiom-20170501/src/algebra/MAPPKG1.spad is in axiom-source 20170501-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 | )abbrev package MAPPKG1 MappingPackage1
++ Author: S.M.Watt and W.H.Burge
++ Date Created:Jan 87
++ Date Last Updated:Feb 92
++ Description:
++ Various Currying operations.
MappingPackage1(A) : SIG == CODE where
A : SetCategory
NNI ==> NonNegativeInteger
SIG ==> with
nullary : A -> (()->A)
++\spad{nullary A} changes its argument into a
++ nullary function.
coerce : A -> (()->A)
++\spad{coerce A} changes its argument into a
++ nullary function.
fixedPoint : (A->A) -> A
++\spad{fixedPoint f} is the fixed point of function \spad{f}.
++ that is, such that \spad{fixedPoint f = f(fixedPoint f)}.
fixedPoint : (List A->List A, Integer) -> List A
++\spad{fixedPoint(f,n)} is the fixed point of function
++ \spad{f} which is assumed to transform a list of length
++ \spad{n}.
id : A -> A
++\spad{id x} is \spad{x}.
"**" : (A->A, NNI) -> (A->A)
++\spad{f**n} is the function which is the n-fold application
++ of \spad{f}.
recur : ((NNI, A)->A) -> ((NNI, A)->A)
++\spad{recur(g)} is the function \spad{h} such that
++ \spad{h(n,x)= g(n,g(n-1,..g(1,x)..))}.
CODE ==> add
MappingPackageInternalHacks1(A)
a: A
faa: A -> A
f0a: ()-> A
nullary a == a
coerce a == nullary a
fixedPoint faa ==
g0 := GENSYM()$Lisp
g1 := faa g0
EQ(g0, g1)$Lisp => error "All points are fixed points"
GEQNSUBSTLIST([g0]$Lisp, [g1]$Lisp, g1)$Lisp
fixedPoint(fll, n) ==
g0 := [(GENSYM()$Lisp):A for i in 1..n]
g1 := fll g0
or/[EQ(e0,e1)$Lisp for e0 in g0 for e1 in g1] =>
error "All points are fixed points"
GEQNSUBSTLIST(g0, g1, g1)$Lisp
-- Composition and recursion.
id a == a
g**n == (a1:A):A +-> iter(g, n, a1)
recur fnaa == (n1:NNI,a2:A):A +-> recur(fnaa, n1, a2)
|