Haskell extraction: c++ functional application

coq2/Extraction.v

+Set Warnings "-notation-overridden,-parsing".
+From sdram Require Export FIFO.
+From Coq Require Extraction.
+Require Import Arith.
+Require Import ExtrHaskellNatNum.
+
+Extraction Language Haskell.
+
+Extract Inductive nat => "Prelude.Int" [ "0" "Prelude.succ" ]
+  "(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))".
+
+Cd "haskell_gencode_orig/".
+Separate Extraction FIFO.
+Cd "..".

coq2/haskell_gencode_orig/App.hs

+module App where
+
+import qualified FIFO
+import qualified Arbiter
+import qualified Bank
+import qualified Commands
+import qualified Datatypes
+import qualified Requests
+import qualified Trace
+import qualified Eqtype
+import qualified Seq
+import qualified Ssrbool
+import qualified Ssrnat
+import qualified Bool
+
+import qualified ForeignRequest
+
+import Foreign
+import Foreign.Storable
+import Foreign.Ptr
+import Foreign.C.String
+import Foreign.C.Types
+
+import System.IO
+import Control.Monad
+
+convertReq :: ForeignRequest.ForeignRequest_t -> IO (Requests.Request_t)
+convertReq r = do
+    case (ForeignRequest.requestType r) of
+        0 -> return (Requests.Coq_mkReq
+            (FIFO.unsafeCoerce(ForeignRequest.requestorID r))
+            (fromIntegral $ ForeignRequest.arriveTime r) 
+            Requests.RD 
+            (fromIntegral $ ForeignRequest.bank r) 
+            (fromIntegral $ ForeignRequest.row r))
+        otherwise ->
+            return (Requests.Coq_mkReq -- write case
+            (FIFO.unsafeCoerce(ForeignRequest.requestorID r))
+            (fromIntegral $ ForeignRequest.arriveTime r) 
+            Requests.WR 
+            (fromIntegral $ ForeignRequest.bank r) 
+            (fromIntegral $ ForeignRequest.row r))
+
+convertReqList :: [ForeignRequest.ForeignRequest_t] -> IO (Datatypes.Coq_list Requests.Request_t)
+convertReqList [] = do return (Datatypes.Coq_nil)
+convertReqList (r:rs) = do
+    coq_req <- convertReq r
+    coq_req_tail <- convertReqList rs
+    return (Datatypes.Coq_cons coq_req coq_req_tail)
+
+--------------------- init state ------------------------------
+fifo_init_state_genstate :: [ForeignRequest.ForeignRequest_t] -> IO (Arbiter.Arbiter_state_t)
+fifo_init_state_genstate reqlist = do
+    coq_list <- convertReqList reqlist
+    -- this should be arguments eventually
+    let bkcfg = Bank.Build_Bank_configuration 1 1 1 1 1 1 1 1 1 1 1 1 1 1
+    let reqcfg = (FIFO.unsafeCoerce CInt)
+    let fifocfg = 10
+    -- calling coq
+    return (FIFO.coq_Init_state bkcfg reqcfg fifocfg coq_list)
+
+foreign export ccall fifo_init_state_wrapper :: CInt -> ForeignRequest.PtrRequest -> IO (StablePtr Arbiter.Arbiter_state_t)
+fifo_init_state_wrapper :: CInt -> ForeignRequest.PtrRequest -> IO (StablePtr Arbiter.Arbiter_state_t)
+fifo_init_state_wrapper size ptr = 
+    if (size == 0) then do
+        reqlist <- return []
+        state <- fifo_init_state_genstate reqlist
+        newStablePtr state
+    else do
+        reqlist <- peekArray (fromIntegral size) ptr
+        state <- fifo_init_state_genstate reqlist
+        newStablePtr state
+---------------------------------------------------------------
+cint2bool :: CInt -> CInt -> Datatypes.Coq_bool
+cint2bool a b =
+    if (a == b) then Datatypes.Coq_true
+    else Datatypes.Coq_false
+
+cint2reflect :: CInt -> CInt -> Bool.Coq_reflect
+cint2reflect a b =
+    if (a == b) then Bool.ReflectT
+    else Bool.ReflectF
+--------------------- next state ------------------------------
+fifo_next_state_genstate :: [ForeignRequest.ForeignRequest_t] -> Arbiter.Arbiter_state_t -> IO (Arbiter.Arbiter_state_t)
+fifo_next_state_genstate reqlist as = do
+    coq_list <- convertReqList reqlist
+    -- this should be arguments eventually
+    let bkcfg = Bank.Build_Bank_configuration 1 1 1 1 1 1 1 1 1 1 1 1 1 1
+    let reqcfg = FIFO.unsafeCoerce ((Eqtype.Equality__Mixin (cint2bool) cint2reflect))
+    let fifocfg = 5
+    -- calling coq
+    return (FIFO.coq_Next_state bkcfg reqcfg fifocfg coq_list as)
+
+foreign export ccall fifo_next_state_wrapper :: CInt -> ForeignRequest.PtrRequest -> StablePtr Arbiter.Arbiter_state_t -> IO (StablePtr Arbiter.Arbiter_state_t)
+fifo_next_state_wrapper :: CInt -> ForeignRequest.PtrRequest -> StablePtr Arbiter.Arbiter_state_t -> IO (StablePtr Arbiter.Arbiter_state_t)
+fifo_next_state_wrapper size ptr as = do
+    case size of
+        0 -> do
+            reqlist <- return []
+            oldstate <- deRefStablePtr as
+            newstate <- fifo_next_state_genstate reqlist oldstate
+            newStablePtr newstate
+        otherwise -> do
+            reqlist <- peekArray (fromIntegral size) ptr
+            oldstate <- deRefStablePtr as
+            newstate <- fifo_next_state_genstate reqlist oldstate
+            newStablePtr newstate
+---------------------------------------------------------------
+
+
+    
+

coq2/haskell_gencode_orig/ForeignRequest.hsc

+module ForeignRequest where
+
+import Foreign
+import Foreign.StablePtr
+import Foreign.Ptr
+import Foreign.C.String
+import Foreign.C.Types
+
+#include "ForeignRequest_t.h"
+
+data ForeignRequest_t = ForeignRequest_t {
+    requestType :: CInt,
+    requestorID :: CUInt,
+    requestSize :: CUInt,
+    address :: CULLong,
+    ddata :: StablePtr CInt,
+    arriveTime :: CUInt,
+    rank :: CUInt,
+    bankGroup :: CUInt,
+    bank :: CUInt,
+    subArray :: CUInt,
+    row :: CUInt,
+    col :: CUInt,
+    addressMap :: CIntPtr
+} deriving (Eq)
+
+type PtrRequest = Ptr ForeignRequest_t
+
+instance Storable ForeignRequest_t where
+    sizeOf    _ = (#size ForeignRequest_t)
+    alignment _ = alignment (undefined :: CInt)
+    peek ptr = do
+        r_type <- (#peek ForeignRequest_t, requestType) ptr
+        r_requestorID <- (#peek ForeignRequest_t, requestorID) ptr
+        r_requestSize <- (#peek ForeignRequest_t, requestSize) ptr
+        r_address <- (#peek ForeignRequest_t, address) ptr
+        r_ddata <- (#peek ForeignRequest_t, ddata) ptr
+        r_arriveTime <- (#peek ForeignRequest_t, arriveTime) ptr
+        r_rank <- (#peek ForeignRequest_t, rank) ptr
+        r_bankGroup <- (#peek ForeignRequest_t, bankGroup) ptr
+        r_bank <- (#peek ForeignRequest_t, bank) ptr
+        r_subArray <- (#peek ForeignRequest_t, subArray) ptr
+        r_row <- (#peek ForeignRequest_t, row) ptr
+        r_col <- (#peek ForeignRequest_t, col) ptr
+        r_addressMap <- (#peek ForeignRequest_t, addressMap) ptr
+        return ForeignRequest_t {
+            requestType = r_type,
+            requestorID = r_requestorID,
+            requestSize = r_requestSize,
+            address = r_address,
+            ddata = r_ddata,
+            arriveTime = r_arriveTime,
+            rank = r_rank,
+            bankGroup = r_bankGroup,
+            bank = r_bank,
+            subArray = r_subArray,
+            row = r_row,
+            col = r_col,
+            addressMap = r_addressMap
+        }
+    poke ptr (ForeignRequest_t requestType requestorID requestSize address ddata arriveTime rank bankGroup bank subArray row col addressMap) = do
+        (#poke ForeignRequest_t, requestType) ptr requestType
+        (#poke ForeignRequest_t, requestorID) ptr requestorID
+        (#poke ForeignRequest_t, requestSize) ptr requestSize
+        (#poke ForeignRequest_t, address) ptr address
+        (#poke ForeignRequest_t, ddata) ptr ddata
+        (#poke ForeignRequest_t, arriveTime) ptr arriveTime
+        (#poke ForeignRequest_t, rank) ptr rank
+        (#poke ForeignRequest_t, bankGroup) ptr bankGroup
+        (#poke ForeignRequest_t, bank) ptr bank
+        (#poke ForeignRequest_t, subArray) ptr subArray
+        (#poke ForeignRequest_t, row) ptr row
+        (#poke ForeignRequest_t, col) ptr col
+        (#poke ForeignRequest_t, addressMap) ptr addressMap
+
+-- foreign export ccall showRequest :: PtrRequest -> IO()
+-- showRequest :: PtrRequest -> IO()
+-- showRequest ptr = do
+--     request <- peek ptr
+--     print (arriveTime request)
\ No newline at end of file

coq2/haskell_gencode_orig/ForeignRequest_t.h

+#ifndef FOREIGNREQUEST_H
+#define FOREIGNREQUEST_H
+
+typedef enum{
+	DATA_READ,
+	DATA_WRITE,
+} RequestType;
+
+typedef struct{
+	RequestType requestType;
+	unsigned int requestorID;
+	unsigned int requestSize;
+	unsigned long long address;
+	void *ddata;
+	unsigned int arriveTime;
+	unsigned int returnTime;
+	unsigned int rank;
+	unsigned int bankGroup;
+	unsigned int bank;
+	unsigned int subArray;
+	unsigned int row;
+	unsigned int col;
+	unsigned int addressMap[4];
+} ForeignRequest_t;
+
+#endif /* REQUEST_H */

coq2/haskell_gencode_orig/MCsimRequest.h

+#ifndef REQUEST_H
+#define REQUEST_H
+
+#include <stdint.h>
+#include <iostream>
+#include <map>
+
+namespace MCsim
+{
+	enum RequestType
+	{
+		DATA_READ,
+		DATA_WRITE,
+	};
+
+	class Request
+	{
+	public:
+		Request(unsigned int id, RequestType requestType, unsigned int size, unsigned long long addr, void *data) : requestType(requestType),
+																													requestorID(id),
+																													requestSize(size),
+																													address(addr),
+																													data(data),
+																													returnTime(0)
+		{
+		}
+		// Fields
+		RequestType requestType;
+		unsigned int requestorID;
+		unsigned int requestSize;
+		unsigned long long address;
+		void *data;
+		unsigned int arriveTime;
+		unsigned int returnTime;
+		unsigned int rank;
+		unsigned int bankGroup;
+		unsigned int bank;
+		unsigned int subArray;
+		unsigned int row;
+		unsigned int col;
+		unsigned int addressMap[4];
+		// Rank, BankGroup, Bank, SubArray
+	};
+} // namespace MCsim
+
+#endif /* REQUEST_H */

coq2/haskell_gencode_orig/README.me

+## C++ application
+
+This is a C++ application that uses the haskell-generated code to run the controller.
+
+You need to have ghc installed, with hsc2hs in it.
+
+1) run 
+```
+./genhaskell.sh
+```
+in the parent folder to copy the generated haskell code into this folder
+
+2) run 
+```
+make main
+```
+in this folder to compile and run the application
\ No newline at end of file

coq2/haskell_gencode_orig/main.cpp

+#include <iostream>
+
+#include "MCsimRequest.h"
+
+#include "ForeignRequest_t.h"
+#include "App_stub.h"
+
+using namespace std;
+
+#define PRINT(str) std::cerr << str << std::endl;
+
+int main(int argc, char *argv[]){
+
+	unsigned long long * data = (unsigned long long *) malloc(sizeof(unsigned long long));
+	* data = 0xDEADBEEF;
+
+	/* This is the C-equivalent request representation */
+	ForeignRequest_t req1 = {
+		DATA_WRITE,	// type
+		1,			// id
+		10,			// size
+		0x0004,		// @
+		data,		// data
+		0,			// arriveTime
+		1,			// returnTime
+		0,			// rank
+		0,			// bankgroup
+		0,			// bank
+		0,			// subArray
+		0,			// row
+		0,			// col
+		{0,1,0,1}	// @ map
+	};
+
+	ForeignRequest_t req2 = {DATA_READ,2,20,0x0008,data,10,20,0,0,1,0,50,0,{1,0,1,0}};
+	ForeignRequest_t req3 = {DATA_READ,3,40,0x000c,data,30,40,0,0,5,0,10,0,{1,0,1,0}};
+	ForeignRequest_t req4 = {DATA_WRITE,4,10,0x0010,data,40,50,0,0,5,0,10,0,{1,0,1,0}};
+
+	ForeignRequest_t reqlist[] = {req1,req2};
+	ForeignRequest_t reqlist2[] = {req3,req4};
+
+	PRINT ("Initializing haskell runtime");
+	hs_init(&argc,&argv);
+	PRINT ("Calling haskell function");
+	// don't know what is inside the pointer
+	void * init_state = fifo_init_state_wrapper(2,&reqlist[0]);
+	void * next_state_1 = fifo_next_state_wrapper(2,&reqlist2[0],init_state);
+	void * next_state_2 = fifo_next_state_wrapper(0,&reqlist[0],next_state_1);
+	void * next_state_3 = fifo_next_state_wrapper(0,&reqlist[0],next_state_2);
+	void * next_state_4 = fifo_next_state_wrapper(0,&reqlist[0],next_state_3);
+	void * next_state_5 = fifo_next_state_wrapper(0,&reqlist[0],next_state_4);
+	void * next_state_6 = fifo_next_state_wrapper(0,&reqlist[0],next_state_5);
+	void * next_state_7 = fifo_next_state_wrapper(0,&reqlist[0],next_state_6);
+	PRINT ("Return from haskell function");
+	hs_exit();
+	PRINT ("Finishing haskell runtime");
+}
\ No newline at end of file

coq2/haskell_gencode_orig/makefile

+OBJ := Nat.o Bool.o Datatypes.o Specif.o Ssrbool.o Fintype.o Eqtype.o Seq.o Bank.o Ssrnat.o Requests.o Commands.o Trace.o Arbiter.o FIFO.o ForeignRequest.o App.o main.o
+
+INCLUDE_DIR := /usr/lib/ghc/include
+
+ForeignRequest.hs : ForeignRequest.hsc
+	hsc2hs $^
+
+App.o: App.hs ForeignRequest.hs
+	ghc $^
+
+main.o: main.cpp
+	g++ -c -I${INCLUDE_DIR} $^ -o $@
+
+main: App.o main.o
+	ghc -no-hs-main ${OBJ} -lstdc++ -o $@
+
+clean:
+	rm -f main *.o *.hi ForeignRequest.hs App_stub.h
\ No newline at end of file