#include io.cam
#include mse.cam
#include sets.cam
#include ffs.cam
#include txt.cam
#include sql.cam

/*****************************************************************************
 *                                                                           *
 *      1. The Specification                                                 *
 *                                                                           *
 *****************************************************************************/

TYPE
        PPD  ::  S: Stock
                 P: Pricelist
                 E: EquipDb;
        Stock  = Unid -> NAT;
        Pricelist = Comp -> Currency;
        EquipDb = Equip -> (Unid -> NAT);
        Unid  = Equip | Comp;
        Comp  :: K: NAT;
        Equip :: K: NAT;
        Currency = NAT;
        NAT = INT;

ENDTYPE

STATE ppd: PPD;

;-----------------------------------------------------------------------------
FUNC Explode(k:Equip):Comp -> NAT
;-----------------------------------------------------------------------------
RETURN explode(k,E(ppd));

;-----------------------------------------------------------------------------
FUNC CompCost(k:Equip,n:NAT):Comp -> NAT
;-----------------------------------------------------------------------------
RETURN let (ms=mseExMul(explode(k,E(ppd)),n))
       in mseDiff(ms,S(ppd));

;-----------------------------------------------------------------------------
FUNC explode(k:Equip,db:EquipDb):Comp -> NAT
;-----------------------------------------------------------------------------
RETURN let (ms=if k in dom(db) then db[k] else [])
       in mseCUP(< if is-Comp(x) then ms / { x }
                                 else mseExMul(explode(x,db \ {k}),ms[x])
                 | x <- dom(ms) >);

;-----------------------------------------------------------------------------
FUNC Init():SYM
;-----------------------------------------------------------------------------
STATE
ppd <- PPD(
[
	Comp(11) -> 10,
	Comp(12) ->  5,
	Comp(13) ->  1,
	Comp(14) -> 20
],
[],
[ 
  Equip( 
     11 )->[ 
       Comp( 
          11 )->1 ,
       Comp( 
          12 )->3  ],
  Equip( 
     12 )->[ 
       Comp( 
          13 )->4 ,
       Equip( 
          11 )->3  ],
  Equip( 
     10 )->[ 
       Equip( 
          11 )->3 ,
       Equip( 
          12 )->2  ] ]);

;-----------------------------------------------------------------------------
; Initialization
;-----------------------------------------------------------------------------
;Init();
;-----------------------------------------------------------------------------

/*****************************************************************************
 *                                                                           *
 *      2. The Reification Process                                           *
 *                                                                           *
 *****************************************************************************/

abs_Unid(x) = let (i=p1(x),y=p2(x)) in if i==2 then Comp(y) else Equip(y);
rep_Unid(x) = < if is-Comp(x) then 2 else 1,K(x)>;

rep0 <- lambda(x).< <(rep_Unid->*)(S(x)), (K->*)(P(x))>,
                   (*->(rep_Unid->*))((K->*)(E(x)))>;

rep1 <- prod(id,uncurry);

rep2 <- prod(id,j606o->*);

rep3 <- prod(id,pJoinInv);

rep4 <- prod(id,prod(mkr,mkr));

rep5 <- prod(id,prod(flat-set,flat-set));

rep6 <- prod(id,prod(seq2ff-set,seq2ff-set));

rep7(t) = do(_ppdSP<-p1(t),
             ioObjSave('_ppdSP,p1(t)),
             ioAfs2awk("_ppdEETable",p1(p2(t)),"%"),
             ioAfs2awk("_ppdECTable",p2(p2(t)),"%")
            );

abs6to0(r)=abs0(abs1(abs2(abs3(abs4(abs5(abs6(r)))))));
rep0to6(a)=rep6(rep5(rep4(rep3(rep2(rep1(rep0(a)))))));

/*****************************************************************************
 *                                                                           *
 *      3. The Implementation (Level 7)                                      *
 *                                                                           *
 *****************************************************************************/

;-----------------------------------------------------------------------------
FUNC Explode7(k:Equip):Comp -> NAT
;-----------------------------------------------------------------------------
RETURN do(
           sh("perl ppdExplode.pl " ++ itoa(K(k))),
           ioAfsPrint(ffsRename([1->"Comp",2->"Qty"],ioAwk2afs("_r","%")))
         );

;-----------------------------------------------------------------------------
FUNC Init7():SYM
;-----------------------------------------------------------------------------
STATE rep7(rep0to6(
PPD(
[
        Comp(11) -> 10,
        Comp(12) ->  5,
        Comp(13) ->  1,
        Comp(14) -> 20
],
[],
[ 
  Equip( 
     11 )->[ 
       Comp( 
          11 )->1 ,
       Comp( 
          12 )->3  ],
  Equip( 
     12 )->[ 
       Comp( 
          13 )->4 ,
       Equip( 
          11 )->3  ],
  Equip( 
     10 )->[ 
       Equip( 
          11 )->3 ,
       Equip( 
          12 )->2  ] ])
));

;-----------------------------------------------------------------------------
FUNC CompCost7(k:Equip,n:NAT):Comp -> NAT
;-----------------------------------------------------------------------------
RETURN do(
           sh("perl ppdExplode.pl " ++ itoa(K(k))),
           sh("awk -f otimes.awk m=" ++ itoa(n) ++ " _r > _tmp0 "),
           princ("\n[ mseExMul successfully performed at UNIX level ]\n"),
           ioObjLoad('_ppdSP),
           let (a=(abs_Unid->*)(p1(_ppdSP)),
                b=ioAwk2afs("_tmp0","%"),
                c=[ Comp(atoi(t[1])) -> atoi(t[2]) | t <- b ])
           in princ("\n[ Refinement memo: mseDiff still at abstract level ]\n",
                    "\nResult is:\n",pp(mseDiff(c,a)),),
           ""
         );