; Adenda ao kernel do Camila  (99.10.22 - lsb)


; Motivacao
; O Camila disponibiliza primitivamente um tipo "record"
; que e' basicamente um produto com componentes identificadas
; e um tipo "union" que corresponde a uma uniao
; disjunta um pouco naive.
; No entanto, nao apenas por razoes pragmaticas, mas tb para
; compor a "categorical picture", muitos de nos recorrem a
; codificaçoes directas do produto e coproduto em Set, ie
; produto cartesiano e uniao disjunta implementada por
; etiquetagem das parcelas. Para esses tipos (binarios) o celebre
; setcat.cam fornece projeccoes (p1, p2), imersoes (i1, i2), extensao
; funtorial (prod e sum) e universais (split e either).
;
; Parece nec, neste contexto, proceder a duas extensoes
; ao kernel do Camila:
;
; a. Mantendo os tipos "record" e "union" existentes,
;    criar os tipos 
;    produto   A * B
;    coproduto A + B
;    (cujos valores sao pares de A e B e pares de 1 e A (2 e B),
;    respectivamente) e seus correspondentes n-arios
;    Propoe-se que, para o caso binario, se "oficializem" as
;    correspondentes algebras em setcat.cam e que estas sejam
;    adaptadas para a versão n-aria
;    (eg, haveria um ssplit e um sprod sobre n-tuplos codificados
;    como sequencias.
;
; b. Garantir que tipos "record" e "union" sejam mapeaveis
;    nos correspondentes produto e coproduto, gerando o interpretador
;    de forma automatica as duas componentes do isomorfismo
;    que se passam a designar por in_X e out_X (X sendo o identificador
;    do "record" ou "union" em causa.
;    Assim
;
;    X = a1:A  a2:B  ----- out_X ----->  XX = A * B
;                    <---- in_X ------
;         caso particular:
;         X = a1:A        ----- out_X ----->  A
;                         <---- in_X ------
;         (uma alternativa talvez menos util seria mapear X em XX = A * NIL ...)
;         (e' nec decidir isto!)
;
;    X = A1 | B1
;    A1 = a1:A
;    B1 = b1:B              ----- out_X ----->  XX = A + B
;                           <---- in_X ------
;
;        caso particular:
;        X = [A1]     ----- out_X ----->  XX = A + NIL
;                     <---- in_X ------
;
;
;   A seguir encontra-se uma "implementacao" destes in e outs que tenta ser
;   apenas uma "concept proof" (o JJ acabara sempre por usar - felizmente -
;   versoes mais trotsquistas), para mostrar como estes isos podem ser
;   definidos uniformente.  Trata-se apenas o caso binario (e unario para
;   o "record").
;
; Resta dizer que o tipo A+B ja existe no Camila desde 98 ...
; Mais ate: admite uma versao "verbose" no estilo 
;                   X = label1:A + label2:B
; que origina pares da forma <label1,a> em vez de <1,a>
; Resta apenas fazer as imersoes "verbose" correspondentes ao i1, i2 usuais.


#include setcat.cam

; ------------------------------------------------------------
; EX1:  "record" vs produto
; ------------------------------------------------------------

TYPE
     E = e1:INT e2:STR;
;    EE = INT * STR;
ENDTYPE

; o  E é automatico
; mas é nec recorrer ao bless para invocar com
; um par uma função --- E --- de dois argumentos

out_E(x) = split(e1,e2)(x);
in_E(x) = bless('E,x);
; JJ: bug no bless?  in_s('E,<33,"ww">) ok mas
;                    ((curry(bless))('E)) (<33,"ww">) da erro

; ------------------------------------------------------------
; EX2: "record" vs tipo simples 
; ------------------------------------------------------------

TYPE
     V = v1:INT;
     VV = INT;
ENDTYPE

out_V(x) = v1(x);
in_V(x) = V(x);

; ------------------------------------------------------------
; EX3: outro exemplo
; ------------------------------------------------------------

TYPE
     T = t1:V t2:E;
;    TT = V * E = INT * (INT * STR);
ENDTYPE

out_T(x) = split(t1,t2)(x);
in_T(x) = bless('T,x);

; ?- out_T(t);
; < 
;   V( 
;      8 ) 
;   E( 
;      12 ,
;      www )>
; ?- prod(out_V,out_E)( out_T(t));
; < 8  < 12  www >>

; os in e outs podem obviamente ser estruturalmente compostos, eg

total_out_T(x) = prod(out_V,out_E)(out_T(x));

; ------------------------------------------------------------
; EX4: "union" vs coproduto
; ------------------------------------------------------------

TYPE
   F = A1 | A2;
   A1 = a1:INT;
   A2 = a2:STR;

   CF = INT + STR;
ENDTYPE

in_F(x) = either(in_A1,in_A2)(x);
out_F(x) = if (is-A1(x) -> i1(out_A1(x)),
               is-A2(x) -> i2(out_A2(x))
              );

in_A1(x) = A1(x);
out_A1(x) = a1(x);
in_A2(x) = A2(x);
out_A2(x) = a2(x);

; ex:
; ?- out_F(A1(8));
; < 1  8 >
; ?- out_F(A2("www"));
; < 2  www >
; ?- in_F(i1(3));
; 
; A1( 
;    3 )

; ------------------------------------------------------------
; EX5: outro exemplo ("recursivo")
; ------------------------------------------------------------

TYPE
	X = Y | Z;
	Y = C1: ANY; 
	Z = C2: ANY C3: X;
ENDTYPE

out_Y(x) = C1(x);
in_Y(x) = Y(x);

out_Z(x) = split(C2,C3)(x);
in_Z(x) = bless('Z,x);

out_X(x) = if (is-Y(x) -> i1(out_Y(x)),
              is-Z(x) -> i2(out_Z(x))
             );

in_X(x) = either(in_Y,in_Z)(x); 

; JJ: MAS o in_Z da erro! Tudo corre bem se usarmos:
in_Z(x) = blessZ(x);
blessZ <- lambda(p).Z(p1(p),p2(p));
; bug no bless?

; ------------------------------------------------------------