;-------------------------------------------------------------------------------
; setcat.cam = a simplistic model of set theory (based one category Set)
;              in CAMILA
;-------------------------------------------------------------------------------
; Creation date : 1999.03.31
; Last update :   1999.04.29
; Last update :   1999.10.22
; (c) UM - M.F.P. II - 1998/99
;-------------------------------------------------------------------------------

;--- (a) Basics ----------------------------------------------------------------

; una is a generic function which converts a binary function into a unary
; function on pairs.
  una(f)=lambda(p).f(p1(p),p2(p));
;;; f(<a,b>)  ->  f'(a,b)

; bin does the opposite of 'una'
  bin(f)=lambda(a,b).f(<a,b>);

; flip permutes the order of arguments of a binary function
  flip(f)=lambda(b,a).f(a,b);

; perm outputs a permutation of finite set s
  perm(s)= < a | a <- s >;

;;; permut
  permut(s)= if(s is-{}    -> {<>},
                s is-<e:r> -> { let(e = hd(x)) in
                                 { <e: x> | x <- permut(r) }| x <- s },
                s is-<e:r> -> { <e: x> | x <- permut(r) },
                s is-{e:r} -> { <e: x> | x <- permut(r) }) ;

; get : B --> A --> (A -> B) --> B 
; get totalizes a partial function (f) with a default value (u)
  get(u)=lambda(a).lambda(f).if a in dom(f) then f[a] else u;
;;; ou entao
  jjget(u)=lambda(a).lambda(f).ap(f,a,u);

eqk(k)= lambda(x).x==k;

inseq(n) = perm(inseg(n));

uplus <- una(plus);

PLUS(s) = plus-orio([],s);

MAX(s) = max-orio(0,s);

selUp(s,f)=lambda(x). x + ((*->f)(x/s));

pred(n)=n.-1;

succ(n)=n.+1;

;--- (b) CCC -------------------------------------------------------------------

; id : A --> A
  id(x)=x;

; comp : (C <-- B) x (B <-- A) --> (C <-- A) 
  comp(f,g)= lambda(x).f(g(x));
;;; NOTA = _comp 

; const : C --> (A --> C)
  const(c)= lambda(x).c;

; excl : A --> 1
  excl <- const(NIL);

; curry : (A x B --> C) --> A --> (B -->C)
  curry(f) = lambda(a).lambda(b).f('a,b);

; i1 : (A + B) <-- A
  i1(a) = <1,a>;

; i2 : (A + B) <-- B
  i2(b) = <2,b>;

; grd : (A --> 2) --> A --> (A + A)
  grd(p) = lambda(x). if p(x) then i1(x) else i2(x);

; is1 : ( A + B ) --> 2
  is1(x) = p1(x)==1;

; is2 : ( A + B ) --> 2
  is2(x) = p1(x)==2;

; split : ( A --> B x C )  <--  ( A --> B ) x ( A --> C )
  split(f,g)= lambda(x).<'f(x),'g(x)>;

; either : (A --> C) x (B --> C) --> ((A + B) --> C)
  either(f,g)=lambda(x).let (t=p1(x),y=p2(x)) in if t==1 then 'f(y) else 'g(y);

; prod : (A --> B) x (C --> D) --> ((A x C) --> (B x D))
  prod(f,g) = split(comp(f,p1),comp(g,p2));

; diag : (A --> B)  --> ((A x A) --> (B x B))
; diag is the diagonal functor construct
  diag(f) = prod(f,f);

; sum : (A --> B) x (C --> D) --> ((A + C) --> (B + D))
  sum(f,g) = either(comp(i1,f),comp(i2,g));

; swap : (A x B) --> (B x A)
  swap <- split(p2,p1);

; assocr : (A x B) x C --> A x (B x C)
  assocr <- split(comp(p1,p1),prod(p2,id));

; assocl : A x (B x C) --> (A x B) x C
  assocl <- split(prod(id,p1),comp(p2,p2));

; pwnil : A --> (A x 1)			/* pwnil = pair with NIL */
  pwnil <- split(id,excl);

; coswap : (A + B) --> (B + A)
  coswap <- either(i2,i1);

; coassocr : ((A + B) + C) --> (A + (B + C))
  coassocr <- either(sum(id,i1),comp(i2,i2));

; undistr : A x ( B + C ) <-- ( ( A x B ) + ( A x C ) )
  undistr <- either(prod(id,i1),prod(id,i2));

; split0 : (A --> 1) <-- 1
  split0 <- lambda(x). const(NIL);

; uneither0 : 1 <-- (0 --> A)
  uneither0 <- lambda(x). NIL;

; untab : ( A -> B ) --> (A -> (B + 1))
  untab(sigma)=comp(sum(curry(ap)(sigma),excl),grd(lambda(a).a in dom(sigma))); 

; cf : ( A --> 2 ) <-- A-set		/* cf = characteristic function */
  cf(s) = lambda(a).a in s;

; pair2exp : ( 2 --> A ) <-- A x A
; an isomorphism
  pair2exp(p) = lambda(b). if b then p2(p) else p1(p);

; nestr : A × B × C  -->  A × (B × C)
  nestr <- split(p1,split(p2,p3));

; nestl : A × B × C  -->  (A × B) × C
  nestl <- split(split(p1,p2),p3);

; flatr : A × (B × C)  -->  A × B × C
  flatr(t)=<p1(t),p1(p2(t)),p2(p2(t))>;

; flatl : (A × B) × C  -->  A × B × C
  flatl(t)=<p1(p1(t)),p2(p1(t)),p2(t)>;

;--- (c) Partial maps ----------------------------------------------------------

; set2fm : ( A -> 1 ) <-- A-set
; dom is the inverse of set2fm
  set2fm(s) = [ x -> NIL | x <- s ];

; peither : ( ( A + B ) -> C )  <--  ( A -> C ) x ( B -> C )
; This is the "partial version" of either
  peither(f1,f2) = (i1->*)(f1) + (i2->*)(f2);

; unpeither : ( ( A + B ) -> C )  -->  ( A -> C ) x ( B -> C )
; The inverse of (unary) unpeither
  unpeither(f) = let (a=[ p2(x) -> f[x] | x <- dom(f): p1(x) == 1 ],
                      b=[ p2(x) -> f[x] | x <- dom(f): p1(x) == 2 ])
                 in < a , b >;

; join : ( A -> B x C )  <--  ( A -> B ) x ( A -> C )
; This is the "partial version" of split
  join(f1,f2) = [ a -> < f1[a],f2[a]> | a <- dom(f1) * dom(f2) ];

join_ <- una(join);

; unjoin : ( A -> B x C )  -->  ( A -> B ) x ( A -> C )
; The right-inverse of join_, ie join_ . unjoin = id.
  unjoin <- split(*->p1,*->p2);

; pcurry : (A x B -> C) --> A -> (B->C)
; pcurry is the "partial version" of curry.
; It is not epic and therefore not iso
  pcurry(f) =
	let (x=dom(f), y=p1-set(x))
	in [ a -> [ p2(p) -> f[p] | p <- x : p1(p)==a ] | a <- y ];

; unpcurry : (A x B -> C) <-- A -> ( B -> C )
; unpcurry is the "partial version" of uncurry.
; It is not monic and therefore not iso
  unpcurry(f) =
       PLUS({ let (g=f[a]) in [ <a,b>  -> g[b] | b <- dom(g) ] | a <- dom(f) });

; collect : (A x B)-set --> A -> B-set
; collect can be calculated from pcurry and set2fm
  collect(r) = [ a -> { p2(q) | q <- r: a==p1(q) } | a <- { p1(p) | p <- r } ];

; discollect : (A x B)-set <-- A -> B-set
; discollect can be calculated from unpcurry and set2fm
  discollect(f) = UNION({ { <a,b> | b <- f[a] } | a <- dom(f) });

; njoin : ((A -> D) x (A x B -> C)) --> (A -> D x (B->C))
; njoin (read: 'nested join') is epic but not mono
  njoin <- comp(join_,split(p1,comp(uplus,prod((*->const([])),pcurry))));

; unnjoin : ((A -> D) x (A x B -> C)) <-- (A -> D x (B->C))
; njoin . unnjoin = id, ie. unnjoin is njoin's right-inverse.
  unnjoin <- comp(prod(id,unpcurry),unjoin);

; cojoin : ( A -> (B + C) )  <--  ( A -> B ) x ( A -> C )
  cojoin(f,g) = let (h=f\dom(g), i=g\dom(f)) in  (*->i1)(h) + (*->i2)(i);

; uncojoin : ( A -> (B + C) )  -->  ( A -> B ) x ( A -> C )
  uncojoin(f) = let (x={ a | a <- dom(f): is1(f[a]) },
		     y={ a | a <- dom(f): is2(f[a]) })
		in  <(*->p2)(f/x),(*->p2)(f/y)>;

; ffinv : (A -> B) --> (B -> A-set)
; ffinv(f) "reverses" f.
  ffinv(f) = [ b -> { a | a<- dom(f): f[a]==b } | b <- ran(f) ];

; unffinv : (A -> B) <-- (B -> A-set)
; unffinv is ffinv's right inverse, that is ffinv . unffinv = id
  unffinv(f)= let (x={ [ a -> b | a <- f[b] ] | b <- dom(f) },
		   y={ f \ UNION(dom-set(x-{f})) | f <- x })
	      in  PLUS([],y);

; mkf :  (A -> B)  <--  (A x B)-set 
; This is partial function !
  mkf <- comp((*->the),collect); /* ie [ p1(t) -> p2(t) | t <- r ] */

; mkr :  (A -> B)  -->  (A x B)-set 
  mkr(f) = { <a,f[a]> | a <- dom(f) };

;--- (d) Sequences -------------------------------------------------------------

; fm2seq : A-seq <-- (NAT -> A)
; Turns a numeric index of A-values into the implicit sequence
  fm2seq(f) =
	 if f==[] then <> else let (m=MAX(dom(f))) in fm2seq(f\{m}) ^ < f[m] >;

; seq2fm : A-seq --> (NAT -> A)
; A sequence is represented by a numerical index keeping track of the original
; order. Right-inverse of fm2seq.
  seq2fm(l) = [ x -> l[x] | x <- inseg(length(l)) ];

; zip  : (B x C)-seq  <--  B-seq  x  C-seq
; This is the "seq version" of join
  zip(l,m) =
	let (n=min(length(l),length(m))) in < < l[i],m[i] > | i <- inseq(n) >;

; unzip  : (B x C)-seq  -->  B-seq  x  C-seq
; The right-inverse of una(zip), ie una(zip) . unzip = id.
  unzip  <- split(p1-seq,p2-seq);

;--- (e) X = 1 + A x X structure hylo ------------------------------------------

inF  <- either(const(<>),una(cons));

outF <- comp(sum(const(nil),split(hd,tl)),grd(eqk(<>)));

recF(f)=sum(id,prod(id,f));

cata(g) = lambda(x).(comp(g,comp(recF(cata(g)),outF)))(x);

ana(g) = lambda(x).(comp(inF,comp(recF(ana(g)),g)))(x);

hylo(h,g) = comp(cata(h),ana(g));

;--- (e.1) application to set-folding ------------------------------------------

; nsetget : A-set --> A x A-set
; nsetget is undefined for the empty set
  nsetget(s) = let (a=choice(s)) in <a,s-{a}>;

; gets : A-set --> 1 + A x A-set
; gets is the A-set standard coalgebra
  gets <- comp(sum(const(NIL),nsetget),grd(eqk({})));

; tot2 : (B x B -> B) x B --> (A x B)-set --> B
; tot2 totalizes a binary relation on the second projection according to
; monoid structure f: B x B -> B and u: B
  tot2(f,u)= hylo(either(const(u),comp(una(f),prod(p2,id))),gets);

;--- (e.2) application to Nat-folding ------------------------------------------

getN <- comp(sum(const(nil),split(id,pred)),grd(eqk(0)));

fac <- hylo(either(const(1),una(mul)),getN);