package Bug675_ModuleCollect_Classic where {

import ModuleCollect;

import List;

import ListN;

import Assert;

interface AssertionWires n = {
    wires :: Bit n ;
    clear :: Action ;
};

interface AssertionWire = {
    index :: Integer ;
    fail :: Bool ;
    clear :: Action ;
};

type AssertModule i = ModuleCollect AssertionWire i;

type CondIfc i n = Tuple2 (AssertionWires n) i;

interface AssertionReg = {
    set :: Action ;
    clear :: Action ;
};

conditionReg :: Integer -> AssertModule AssertionReg;
conditionReg ix =
    module {
      cond :: Reg Bool <- mkReg False;
      let { item' =
              interface AssertionWire {
                index =  ix;;
                fail =  cond;;
                clear :: Action;
                clear =  action { cond := False; };
              };
          };
      let { item =  item'; };
      addToCollection item;
      interface {
        set :: Action;
        set =  action { cond := True; };;
        clear :: Action;
        clear =  action { cond := False; };
      }
    };;

readCond :: AssertionWire -> Bool;
readCond c =  c.fail;;

exposeAssertionWires :: AssertModule i -> Module (CondIfc i n);
exposeAssertionWires mkI =
    module {
      ecs :: IWithCollection AssertionWire i <- exposeCollection mkI;
      let { cs' =  ecs.collection; };
      let { cs =  cs'; };
      theResult' <-
          do { let { i' :: Integer;
                     i' =  0; };
               let { i :: Integer;
                     i =  i'; };
               let { f' :: (IsModule m' c) => Integer -> m' Integer;
                     f' i = if i < length cs then
                                do { staticAssert
                                         ((primSelectFn _ cs i).index <
                                             primValueOf (_::(Bit n)))
                                            "Assertion index out of range";
                                     let { i' :: Integer;
                                           i' =  i + 1; };
                                     let { i :: Integer;
                                           i =  i'; };
                                     f' i;
                                   }
                            else
                                do { Prelude.return i; };
                    };
               theResult' <- f' i;
               let { i =  theResult'; };
               return ();
             };
      let { () =  theResult'; };
      let { c_ifc' :: AssertionWires m;
            c_ifc' =
              interface AssertionWires {
                wires =
                    let xs' :: ListN n Bool;
                        xs' =  map readCond (toListN cs);
                    in  let xs :: ListN n Bool;
                            xs =  xs';
                        in  pack xs;;
                clear :: Action;
                clear =
                  action {
                    let { i' :: Integer;
                          i' =  0; };
                    let { i :: Integer;
                          i =  i'; };
                    let { f' :: Integer -> ActionValue Integer;
                          f' i = if i < primValueOf (_::(Bit n)) then
                                     do { (primSelectFn _ cs i).clear;
                                          let { i' :: Integer;
                                                i' =  i +  1; };
                                          let { i :: Integer;
                                                i =  i'; };
                                          f' i;
                                        }
                                 else
                                     do { return i; };
                        };
                    theResult' <- f' i;
                    let { i =  theResult'; };
                  };
              };
          };
      let { c_ifc :: AssertionWires m;
            c_ifc =  c_ifc'; };
      let { dut_ifc' =  ecs.device; };
      let { dut_ifc =  dut_ifc'; };
      return (tuple2 c_ifc dut_ifc);
    };
}