Skip to content
Snippets Groups Projects
Commit 5e91ea7e authored by Felipe Lisboa's avatar Felipe Lisboa
Browse files

Haskell extraction, printable version

parent accb8140
No related branches found
No related tags found
No related merge requests found
Showing
with 1233 additions and 0 deletions
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
---------------------------------------------------------------
------------------------------------------------------------------------------------------
-- output functions
------------------------------------------------------------------------------------------
req2string :: Requests.Request_t -> String
req2string req =
"requestor: " ++ show(FIFO.unsafeCoerce(Requests.requestor req) :: CInt) ++
", date: " ++ show(Requests.date req) ++
", type: " ++ show(Requests.typ req) ++
", bank: " ++ show(Requests.bank req) ++
", row: " ++ show(Requests.row req)
print_command :: Commands.Command_t -> IO()
print_command cmd = do
case Commands.kind cmd of
Commands.ACT ->
putStr $ show(Commands.date cmd) ++ ", ACT. Request: " ++
req2string (Commands.request cmd)
Commands.PRE ->
putStr $ show(Commands.date cmd) ++ ", PRE. Request: " ++
req2string (Commands.request cmd)
Commands.CRD ->
putStr $ show(Commands.date cmd) ++ ", RD. Request: " ++
req2string (Commands.request cmd)
Commands.CWR ->
putStr $ show(Commands.date cmd) ++ ", WR. Request: " ++
req2string (Commands.request cmd)
print_cmd_list :: Datatypes.Coq_list Commands.Command_t -> IO()
print_cmd_list Datatypes.Coq_nil = putStrLn "[::]"
print_cmd_list (Datatypes.Coq_cons hd tail) = do
putStr "["
print_command hd
putStr "],"
print_cmd_list tail
print_req_list :: Datatypes.Coq_list Requests.Request_t -> IO()
print_req_list Datatypes.Coq_nil = putStrLn "[::]"
print_req_list (Datatypes.Coq_cons hd tail) = do
putStr "["
putStr $ req2string hd
putStr "],"
print_req_list tail
foreign export ccall print_state :: StablePtr Arbiter.Arbiter_state_t -> IO()
print_state :: StablePtr Arbiter.Arbiter_state_t -> IO()
print_state ptr = do
state <- deRefStablePtr ptr
putStrLn "------------------- printing state -------------------"
print_cmd_list (Arbiter.cmds state)
print $ "Time: " ++ show (Arbiter.time state)
let fifo_state = (FIFO.unsafeCoerce(Arbiter.internal_state state) :: FIFO.FIFO_state_t)
case fifo_state of
FIFO.IDLE c p -> do
putStrLn $ "IDLE, Counter: " ++ show(c)
putStr $ "Pending List: "
print_req_list p
FIFO.RUNNING c p r -> do
putStrLn $ "RUNNING, Counter: " ++ show(c)
putStrLn $ "Request being currently served: " ++ req2string r
putStr $ "Pending List: "
print_req_list p
putStrLn "------------------------------------------------------"
------------------------------------------------------------------------------------------
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Arbiter where
import qualified Prelude
import qualified Bank
import qualified Commands
import qualified Datatypes
import qualified Requests
import qualified Trace
import qualified Eqtype
import qualified Seq
import qualified Ssrnat
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif
type Arrival_function_t =
Prelude.Int -> Requests.Requests_t
-- singleton inductive, whose constructor was mkArrivalFunction
coq_Arrival_at :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Arrival_function_t ->
Prelude.Int -> Requests.Requests_t
coq_Arrival_at _ _ arrival_function_t =
arrival_function_t
data Arbiter_state_t = Coq_mkArbiterState {
cmds :: Commands.Commands_t,
time :: Prelude.Int,
internal_state :: Bank.State_t
}
coq_Arbiter_Commands :: Bank.Requestor_configuration -> Bank.Arbiter_configuration ->
Bank.Bank_configuration -> Arbiter_state_t -> Commands.Commands_t
coq_Arbiter_Commands _ _ _ a =
case a of {
Coq_mkArbiterState arbiter_Commands _ _ -> arbiter_Commands}
coq_Arbiter_Time :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration
-> Arbiter_state_t -> Prelude.Int
coq_Arbiter_Time _ _ _ a =
case a of {
Coq_mkArbiterState _ arbiter_Time _ -> arbiter_Time}
coq_Arbiter_State :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration
-> Arbiter_state_t -> Bank.State_t
coq_Arbiter_State _ _ _ a =
case a of {
Coq_mkArbiterState _ _ arbiter_State -> arbiter_State}
data Arbiter_trace_t =
Coq_mkArbiterTrace (Requests.Requests_t -> Arbiter_state_t) (Requests.Requests_t -> Arbiter_state_t ->
Arbiter_state_t)
coq_Init :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration ->
Arbiter_trace_t -> Requests.Requests_t -> Arbiter_state_t
coq_Init _ _ _ arbiter_trace_t =
case arbiter_trace_t of {
Coq_mkArbiterTrace init _ -> init}
coq_Next :: Bank.Requestor_configuration -> Bank.Arbiter_configuration -> Bank.Bank_configuration ->
Arbiter_trace_t -> Requests.Requests_t -> Arbiter_state_t -> Arbiter_state_t
coq_Next _ _ _ arbiter_trace_t =
case arbiter_trace_t of {
Coq_mkArbiterTrace _ next -> next}
type Arbiter_t = Prelude.Int -> Trace.Trace_t
-- singleton inductive, whose constructor was mkArbiter
coq_Default_arrival_at :: Bank.Requestor_configuration -> Bank.Bank_configuration -> (Datatypes.Coq_list
Requests.Request_t) -> Eqtype.Equality__Coq_sort -> Datatypes.Coq_list
Requests.Request_t
coq_Default_arrival_at rEQESTOR_CFG bANK_CFG input t =
Seq.filter (\x ->
Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce Requests.coq_Date rEQESTOR_CFG bANK_CFG x) t) input
coq_Default_arrival_function_t :: Bank.Requestor_configuration -> Bank.Bank_configuration ->
Requests.Requests_t -> Arrival_function_t
coq_Default_arrival_function_t rEQESTOR_CFG bANK_CFG r =
unsafeCoerce coq_Default_arrival_at rEQESTOR_CFG bANK_CFG r
coq_Default_arbitrate :: Bank.Requestor_configuration -> Bank.Arbiter_configuration ->
Bank.Bank_configuration -> Arrival_function_t -> Arbiter_trace_t -> Prelude.Int
-> Arbiter_state_t
coq_Default_arbitrate rEQESTOR_CFG aRBITER_CFG bANK_CFG aF aT t =
let {r = coq_Arrival_at rEQESTOR_CFG bANK_CFG aF t} in
(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
(\_ -> coq_Init rEQESTOR_CFG aRBITER_CFG bANK_CFG aT r)
(\t' ->
coq_Next rEQESTOR_CFG aRBITER_CFG bANK_CFG aT r
(coq_Default_arbitrate rEQESTOR_CFG aRBITER_CFG bANK_CFG aF aT t'))
t
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Bank where
import qualified Prelude
import qualified Eqtype
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif
type Row_t = Prelude.Int
type Requestor_configuration =
Eqtype.Equality__Coq_type
-- singleton inductive, whose constructor was Build_Requestor_configuration
coq_Requestor_t :: Requestor_configuration -> Eqtype.Equality__Coq_type
coq_Requestor_t requestor_configuration =
requestor_configuration
data Arbiter_configuration =
Build_Arbiter_configuration
type State_t = Any
data Bank_configuration =
Build_Bank_configuration Prelude.Int Prelude.Int Prelude.Int Prelude.Int Prelude.Int Prelude.Int
Prelude.Int Prelude.Int Prelude.Int Prelude.Int Prelude.Int Prelude.Int Prelude.Int Prelude.Int
coq_BANKS :: Bank_configuration -> Prelude.Int
coq_BANKS bank_configuration =
case bank_configuration of {
Build_Bank_configuration bANKS _ _ _ _ _ _ _ _ _ _ _ _ _ -> bANKS}
coq_T_RP :: Bank_configuration -> Prelude.Int
coq_T_RP bank_configuration =
case bank_configuration of {
Build_Bank_configuration _ _ _ _ _ _ t_RP _ _ _ _ _ _ _ -> t_RP}
coq_T_RCD :: Bank_configuration -> Prelude.Int
coq_T_RCD bank_configuration =
case bank_configuration of {
Build_Bank_configuration _ _ _ _ _ _ _ t_RCD _ _ _ _ _ _ -> t_RCD}
type Bank_t = Prelude.Int
module Bool where
import qualified Prelude
data Coq_reflect =
ReflectT
| ReflectF
module Commands where
import qualified Prelude
import qualified Bank
import qualified Datatypes
import qualified Requests
data Command_kind_t =
ACT
| PRE
| CRD
| CWR
data Command_t = Coq_mkCmd {
date :: Prelude.Int,
kind :: Command_kind_t,
request :: Requests.Request_t
}
coq_Kind_of_req :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Requests.Request_t ->
Command_kind_t
coq_Kind_of_req rEQESTOR_CFG bANK_CFG req =
case Requests.coq_Kind rEQESTOR_CFG bANK_CFG req of {
Requests.RD -> CRD;
Requests.WR -> CWR}
coq_PRE_of_req :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Requests.Request_t ->
Prelude.Int -> Command_t
coq_PRE_of_req _ _ req t =
Coq_mkCmd t PRE req
coq_ACT_of_req :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Requests.Request_t ->
Prelude.Int -> Command_t
coq_ACT_of_req _ _ req t =
Coq_mkCmd t ACT req
coq_CAS_of_req :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Requests.Request_t ->
Prelude.Int -> Command_t
coq_CAS_of_req rEQESTOR_CFG bANK_CFG req t =
Coq_mkCmd t (coq_Kind_of_req rEQESTOR_CFG bANK_CFG req) req
type Commands_t = Datatypes.Coq_list Command_t
module Datatypes where
import qualified Prelude
data Coq_unit =
Coq_tt
data Coq_bool =
Coq_true
| Coq_false
andb :: Coq_bool -> Coq_bool -> Coq_bool
andb b1 b2 =
case b1 of {
Coq_true -> b2;
Coq_false -> Coq_false}
data Coq_list a =
Coq_nil
| Coq_cons a (Coq_list a)
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Eqtype where
import qualified Prelude
import qualified Bool
import qualified Datatypes
import qualified Specif
import qualified Ssrbool
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif
#ifdef __GLASGOW_HASKELL__
type Any = GHC.Base.Any
#else
-- HUGS
type Any = ()
#endif
__ :: any
__ = Prelude.error "Logical or arity value used"
type Equality__Coq_axiom t = t -> t -> Bool.Coq_reflect
data Equality__Coq_mixin_of t =
Equality__Mixin (Ssrbool.Coq_rel t) (Equality__Coq_axiom t)
_Equality__op :: (Equality__Coq_mixin_of a1) -> Ssrbool.Coq_rel a1
_Equality__op m =
case m of {
Equality__Mixin op0 _ -> op0}
type Equality__Coq_type = Equality__Coq_mixin_of Any
-- singleton inductive, whose constructor was Pack
type Equality__Coq_sort = Any
_Equality__coq_class :: Equality__Coq_type -> Equality__Coq_mixin_of Equality__Coq_sort
_Equality__coq_class cT =
cT
eq_op :: Equality__Coq_type -> Ssrbool.Coq_rel Equality__Coq_sort
eq_op t =
_Equality__op (_Equality__coq_class t)
eqP :: Equality__Coq_type -> Equality__Coq_axiom Equality__Coq_sort
eqP t =
let {_evar_0_ = \_ a -> a} in case t of {
Equality__Mixin x x0 -> _evar_0_ x x0}
unit_eqP :: Equality__Coq_axiom Datatypes.Coq_unit
unit_eqP _ _ =
Bool.ReflectT
unit_eqMixin :: Equality__Coq_mixin_of Datatypes.Coq_unit
unit_eqMixin =
Equality__Mixin (\_ _ -> Datatypes.Coq_true) unit_eqP
unit_eqType :: Equality__Coq_type
unit_eqType =
unsafeCoerce unit_eqMixin
data Coq_subType t =
SubType (Any -> t) (t -> () -> Any) (() -> (t -> () -> Any) -> Any -> Any)
type Coq_sub_sort t = Any
val :: (Ssrbool.Coq_pred a1) -> (Coq_subType a1) -> (Coq_sub_sort a1) -> a1
val _ s =
case s of {
SubType val0 _ _ -> val0}
sig_subType :: (Ssrbool.Coq_pred a1) -> Coq_subType a1
sig_subType _ =
SubType (unsafeCoerce Specif.proj1_sig) (unsafeCoerce (\x _ -> x)) (\_ k_S u -> k_S (unsafeCoerce u) __)
inj_eqAxiom :: Equality__Coq_type -> (a1 -> Equality__Coq_sort) -> Equality__Coq_axiom a1
inj_eqAxiom eT f x y =
Ssrbool.iffP (eq_op eT (f x) (f y)) (eqP eT (f x) (f y))
val_eqP :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) -> (Coq_subType Equality__Coq_sort)
-> Equality__Coq_axiom (Coq_sub_sort Equality__Coq_sort)
val_eqP t p sT =
inj_eqAxiom t (val p sT)
sig_eqMixin :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) -> Equality__Coq_mixin_of
Equality__Coq_sort
sig_eqMixin t p =
Equality__Mixin (\x y -> eq_op t (Specif.proj1_sig x) (Specif.proj1_sig y))
(unsafeCoerce val_eqP t p (sig_subType p))
sig_eqType :: Equality__Coq_type -> (Ssrbool.Coq_pred Equality__Coq_sort) -> Equality__Coq_type
sig_eqType t p =
unsafeCoerce sig_eqMixin t p
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module FIFO where
import qualified Prelude
import qualified Arbiter
import qualified Bank
import qualified Commands
import qualified Datatypes
import qualified Nat
import qualified Requests
import qualified Trace
import qualified Eqtype
import qualified Fintype
import qualified Seq
import qualified Ssrnat
import Foreign.C.Types
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif
coq_ACT_date :: Bank.Bank_configuration -> Prelude.Int
coq_ACT_date bANK_CFG =
Nat.pred (Bank.coq_T_RP bANK_CFG)
coq_CAS_date :: Bank.Bank_configuration -> Prelude.Int
coq_CAS_date bANK_CFG =
Ssrnat.addn (coq_ACT_date bANK_CFG) (Bank.coq_T_RCD bANK_CFG)
type FIFO_configuration =
Prelude.Int
-- singleton inductive, whose constructor was Build_FIFO_configuration
coq_WAIT :: Bank.Bank_configuration -> FIFO_configuration -> Prelude.Int
coq_WAIT _ fIFO_configuration =
fIFO_configuration
type Counter_t = Fintype.Coq_ordinal
data FIFO_state_t =
IDLE Counter_t Requests.Requests_t
| RUNNING Counter_t Requests.Requests_t Requests.Request_t
coq_ARBITER_CFG :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Bank.Arbiter_configuration
coq_ARBITER_CFG _ _ _ =
Bank.Build_Arbiter_configuration
coq_OCycle0 :: Bank.Bank_configuration -> FIFO_configuration -> Fintype.Coq_ordinal
coq_OCycle0 _ _ =
0
coq_OACT_date :: Bank.Bank_configuration -> FIFO_configuration -> Fintype.Coq_ordinal
coq_OACT_date bANK_CFG _ =
coq_ACT_date bANK_CFG
coq_OCAS_date :: Bank.Bank_configuration -> FIFO_configuration -> Fintype.Coq_ordinal
coq_OCAS_date bANK_CFG _ =
coq_CAS_date bANK_CFG
coq_Next_cycle :: Bank.Bank_configuration -> FIFO_configuration -> Counter_t -> Counter_t
coq_Next_cycle bANK_CFG fIFO_CFG c =
let {
nextc = Ssrnat.leq (Prelude.succ (Prelude.succ (Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c)))
(coq_WAIT bANK_CFG fIFO_CFG)}
in
case nextc of {
Datatypes.Coq_true -> Prelude.succ (Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c);
Datatypes.Coq_false -> coq_OCycle0 bANK_CFG fIFO_CFG}
coq_Enqueue :: Bank.Bank_configuration -> Bank.Requestor_configuration -> Requests.Requests_t ->
Requests.Requests_t -> Datatypes.Coq_list Requests.Request_t
coq_Enqueue _ _ =
Seq.cat
coq_Dequeue :: Bank.Bank_configuration -> Bank.Requestor_configuration -> Eqtype.Equality__Coq_sort ->
Requests.Requests_t -> Datatypes.Coq_list Eqtype.Equality__Coq_sort
coq_Dequeue bANK_CFG rEQESTOR_CFG r p =
Seq.rem (Requests.coq_Request_eqType rEQESTOR_CFG bANK_CFG) r (unsafeCoerce p)
-- coq_Init_state :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
-- Requests.Requests_t -> Arbiter.Arbiter_state_t
-- coq_Init_state bANK_CFG rEQESTOR_CFG fIFO_CFG r =
-- Arbiter.Coq_mkArbiterState (Datatypes.Coq_cons (Commands.Coq_mkCmd 0 Commands.ACT (Requests.Coq_mkReq (unsafeCoerce CInt) 0 Requests.RD 1 1)) Datatypes.Coq_nil) 0
-- (unsafeCoerce (IDLE (coq_OCycle0 bANK_CFG fIFO_CFG)
-- (coq_Enqueue bANK_CFG rEQESTOR_CFG r Datatypes.Coq_nil)))
coq_Init_state :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Requests.Requests_t -> Arbiter.Arbiter_state_t
coq_Init_state bANK_CFG rEQESTOR_CFG fIFO_CFG r =
Arbiter.Coq_mkArbiterState Datatypes.Coq_nil 0
(unsafeCoerce (IDLE (coq_OCycle0 bANK_CFG fIFO_CFG)
(coq_Enqueue bANK_CFG rEQESTOR_CFG r Datatypes.Coq_nil)))
coq_Next_state :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Requests.Requests_t -> Arbiter.Arbiter_state_t -> Arbiter.Arbiter_state_t
coq_Next_state bANK_CFG rEQESTOR_CFG fIFO_CFG r aS =
let {
cmds = Arbiter.coq_Arbiter_Commands rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG)
bANK_CFG aS}
in
let {
t = Prelude.succ
(Arbiter.coq_Arbiter_Time rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG aS)}
in
let {
s = Arbiter.coq_Arbiter_State rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG aS}
in
case unsafeCoerce s of {
IDLE c p ->
let {c' = coq_Next_cycle bANK_CFG fIFO_CFG c} in
let {p' = coq_Enqueue bANK_CFG rEQESTOR_CFG r p} in
case p of {
Datatypes.Coq_nil -> Arbiter.Coq_mkArbiterState cmds t (unsafeCoerce (IDLE c' p'));
Datatypes.Coq_cons r0 _ -> Arbiter.Coq_mkArbiterState (Datatypes.Coq_cons
(Commands.coq_PRE_of_req rEQESTOR_CFG bANK_CFG r0 t) cmds) t
(unsafeCoerce (RUNNING (coq_OCycle0 bANK_CFG fIFO_CFG)
(unsafeCoerce coq_Dequeue bANK_CFG rEQESTOR_CFG r0 p') r0))};
RUNNING c p r0 ->
let {p' = coq_Enqueue bANK_CFG rEQESTOR_CFG r p} in
let {c' = coq_Next_cycle bANK_CFG fIFO_CFG c} in
case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c)
(unsafeCoerce Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG)
(coq_OACT_date bANK_CFG fIFO_CFG)) of {
Datatypes.Coq_true ->
let {cmds' = Datatypes.Coq_cons (Commands.coq_ACT_of_req rEQESTOR_CFG bANK_CFG r0 t) cmds} in
Arbiter.Coq_mkArbiterState cmds' t (unsafeCoerce (RUNNING c' p' r0));
Datatypes.Coq_false ->
case Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c)
(unsafeCoerce Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG)
(coq_OCAS_date bANK_CFG fIFO_CFG)) of {
Datatypes.Coq_true ->
let {cmds' = Datatypes.Coq_cons (Commands.coq_CAS_of_req rEQESTOR_CFG bANK_CFG r0 t) cmds} in
Arbiter.Coq_mkArbiterState cmds' t (unsafeCoerce (RUNNING c' p' r0));
Datatypes.Coq_false ->
case Eqtype.eq_op Ssrnat.nat_eqType
(unsafeCoerce Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c)
(unsafeCoerce Nat.pred (coq_WAIT bANK_CFG fIFO_CFG)) of {
Datatypes.Coq_true ->
case p of {
Datatypes.Coq_nil -> Arbiter.Coq_mkArbiterState cmds t (unsafeCoerce (IDLE c' p'));
Datatypes.Coq_cons r1 _ -> Arbiter.Coq_mkArbiterState (Datatypes.Coq_cons
(Commands.coq_PRE_of_req rEQESTOR_CFG bANK_CFG r1 t) cmds) t
(unsafeCoerce (RUNNING c' (unsafeCoerce coq_Dequeue bANK_CFG rEQESTOR_CFG r1 p') r1))};
Datatypes.Coq_false -> Arbiter.Coq_mkArbiterState cmds t (unsafeCoerce (RUNNING c' p' r0))}}}}
coq_FIFO_counter :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Arbiter.Arbiter_state_t -> Prelude.Int
coq_FIFO_counter bANK_CFG rEQESTOR_CFG fIFO_CFG aS =
case unsafeCoerce Arbiter.coq_Arbiter_State rEQESTOR_CFG
(coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG aS of {
IDLE c _ -> Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c;
RUNNING c _ _ -> Fintype.nat_of_ord (coq_WAIT bANK_CFG fIFO_CFG) c}
coq_ACommand_t :: Bank.Bank_configuration -> Bank.Requestor_configuration -> Commands.Command_t
coq_ACommand_t =
Prelude.error "AXIOM TO BE REALIZED"
coq_FIFO_arbiter_trace :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Arbiter.Arbiter_trace_t
coq_FIFO_arbiter_trace bANK_CFG rEQESTOR_CFG fIFO_CFG =
Arbiter.Coq_mkArbiterTrace (coq_Init_state bANK_CFG rEQESTOR_CFG fIFO_CFG)
(coq_Next_state bANK_CFG rEQESTOR_CFG fIFO_CFG)
isRUNNING :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Arbiter.Arbiter_state_t -> Datatypes.Coq_bool
isRUNNING bANK_CFG rEQESTOR_CFG fIFO_CFG aS =
case unsafeCoerce Arbiter.coq_Arbiter_State rEQESTOR_CFG
(coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG aS of {
IDLE _ _ -> Datatypes.Coq_false;
RUNNING _ _ _ -> Datatypes.Coq_true}
isIDLE :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Arbiter.Arbiter_state_t -> Datatypes.Coq_bool
isIDLE bANK_CFG rEQESTOR_CFG fIFO_CFG aS =
case unsafeCoerce Arbiter.coq_Arbiter_State rEQESTOR_CFG
(coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG aS of {
IDLE _ _ -> Datatypes.Coq_true;
RUNNING _ _ _ -> Datatypes.Coq_false}
coq_FIFO_arbitrate :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Arbiter.Arrival_function_t -> Prelude.Int -> Trace.Trace_t
coq_FIFO_arbitrate bANK_CFG rEQESTOR_CFG fIFO_CFG aF t =
Trace.Coq_mkTrace
(Arbiter.coq_Arbiter_Commands rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG
(Arbiter.coq_Default_arbitrate rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG)
bANK_CFG aF (coq_FIFO_arbiter_trace bANK_CFG rEQESTOR_CFG fIFO_CFG) t))
(Arbiter.coq_Arbiter_Time rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG) bANK_CFG
(Arbiter.coq_Default_arbitrate rEQESTOR_CFG (coq_ARBITER_CFG bANK_CFG rEQESTOR_CFG fIFO_CFG)
bANK_CFG aF (coq_FIFO_arbiter_trace bANK_CFG rEQESTOR_CFG fIFO_CFG) t))
coq_FIFO_arbiter :: Bank.Bank_configuration -> Bank.Requestor_configuration -> FIFO_configuration ->
Arbiter.Arrival_function_t -> Arbiter.Arbiter_t
coq_FIFO_arbiter =
coq_FIFO_arbitrate
coq_BANK_CFG :: Bank.Bank_configuration
coq_BANK_CFG =
Bank.Build_Bank_configuration (Prelude.succ 0) (Prelude.succ 0) (Prelude.succ 0) (Prelude.succ
(Prelude.succ (Prelude.succ 0))) (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ 0)))))))))))))))))))) (Prelude.succ (Prelude.succ (Prelude.succ 0))) (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ 0)))) (Prelude.succ (Prelude.succ 0)) (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ 0)))) (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ 0)))) (Prelude.succ 0) (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ 0))))))))))
(Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ 0)))))))))) (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ 0))))))))))))
coq_FIFO_CFG :: FIFO_configuration
coq_FIFO_CFG =
Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ (Prelude.succ
(Prelude.succ (Prelude.succ (Prelude.succ 0)))))))))
coq_REQESTOR_CFG :: Bank.Requestor_configuration
coq_REQESTOR_CFG =
Eqtype.unit_eqType
coq_Req1 :: Requests.Request_t
coq_Req1 =
Requests.Coq_mkReq (unsafeCoerce Datatypes.Coq_tt) (Prelude.succ 0) Requests.RD 0 (Prelude.succ 0)
coq_Req2 :: Requests.Request_t
coq_Req2 =
Requests.Coq_mkReq (unsafeCoerce Datatypes.Coq_tt) (Prelude.succ (Prelude.succ 0)) Requests.RD 0
(Prelude.succ 0)
coq_Input :: Requests.Requests_t
coq_Input =
Datatypes.Coq_cons coq_Req2 (Datatypes.Coq_cons coq_Req1 Datatypes.Coq_nil)
coq_AF :: Arbiter.Arrival_function_t
coq_AF =
Arbiter.coq_Default_arrival_function_t coq_REQESTOR_CFG coq_BANK_CFG coq_Input
module Fintype where
import qualified Prelude
type Coq_ordinal = Prelude.Int
-- singleton inductive, whose constructor was Ordinal
nat_of_ord :: Prelude.Int -> Coq_ordinal -> Prelude.Int
nat_of_ord _ i =
i
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
#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 */
#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 */
module Nat where
import qualified Prelude
pred :: Prelude.Int -> Prelude.Int
pred = (\n -> Prelude.max 0 (Prelude.pred n))
sub :: Prelude.Int -> Prelude.Int -> Prelude.Int
sub = (\n m -> Prelude.max 0 (n Prelude.- m))
This version is like the other one, but some output functions were added in the haskell side.
For that, the code generated by coq had to be changed so that the data structures and written in record syntax.
\ No newline at end of file
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Requests where
import qualified Prelude
import qualified Bank
import qualified Bool
import qualified Datatypes
import qualified Eqtype
import qualified Ssrnat
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif
data Request_kind_t =
RD
| WR deriving (Prelude.Show)
coq_Request_kind_eqdef :: Request_kind_t -> Request_kind_t -> Datatypes.Coq_bool
coq_Request_kind_eqdef a b =
case a of {
RD -> case b of {
RD -> Datatypes.Coq_true;
WR -> Datatypes.Coq_false};
WR -> case b of {
RD -> Datatypes.Coq_false;
WR -> Datatypes.Coq_true}}
coq_Request_kind_eqn :: Eqtype.Equality__Coq_axiom Request_kind_t
coq_Request_kind_eqn x y =
let {b = coq_Request_kind_eqdef x y} in
case b of {
Datatypes.Coq_true -> Bool.ReflectT;
Datatypes.Coq_false -> Bool.ReflectF}
coq_Request_kind_eqMixin :: Eqtype.Equality__Coq_mixin_of Request_kind_t
coq_Request_kind_eqMixin =
Eqtype.Equality__Mixin coq_Request_kind_eqdef coq_Request_kind_eqn
coq_Request_kind_eqType :: Eqtype.Equality__Coq_type
coq_Request_kind_eqType =
unsafeCoerce coq_Request_kind_eqMixin
data Request_t = Coq_mkReq {
requestor :: Eqtype.Equality__Coq_sort,
date :: Prelude.Int,
typ :: Request_kind_t,
bank :: Bank.Bank_t,
row :: Bank.Row_t
}
coq_Requestor :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Request_t ->
Eqtype.Equality__Coq_sort
coq_Requestor _ _ r =
case r of {
Coq_mkReq requestor _ _ _ _ -> requestor}
coq_Date :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Request_t -> Prelude.Int
coq_Date _ _ r =
case r of {
Coq_mkReq _ date _ _ _ -> date}
coq_Kind :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Request_t -> Request_kind_t
coq_Kind _ _ r =
case r of {
Coq_mkReq _ _ kind _ _ -> kind}
coq_Bank :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Request_t -> Bank.Bank_t
coq_Bank _ _ r =
case r of {
Coq_mkReq _ _ _ bank _ -> bank}
coq_Row :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Request_t -> Bank.Row_t
coq_Row _ _ r =
case r of {
Coq_mkReq _ _ _ _ row -> row}
coq_Request_eqdef :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Request_t -> Request_t ->
Datatypes.Coq_bool
coq_Request_eqdef rEQESTOR_CFG bANK_CFG a b =
Datatypes.andb
(Datatypes.andb
(Datatypes.andb
(Datatypes.andb
(Eqtype.eq_op (Bank.coq_Requestor_t rEQESTOR_CFG) (coq_Requestor rEQESTOR_CFG bANK_CFG a)
(coq_Requestor rEQESTOR_CFG bANK_CFG b))
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce coq_Date rEQESTOR_CFG bANK_CFG a)
(unsafeCoerce coq_Date rEQESTOR_CFG bANK_CFG b)))
(Eqtype.eq_op coq_Request_kind_eqType (unsafeCoerce coq_Kind rEQESTOR_CFG bANK_CFG a)
(unsafeCoerce coq_Kind rEQESTOR_CFG bANK_CFG b)))
(Eqtype.eq_op
(Eqtype.sig_eqType Ssrnat.nat_eqType (\a0 ->
Ssrnat.leq (Prelude.succ (unsafeCoerce a0)) (Bank.coq_BANKS bANK_CFG)))
(unsafeCoerce coq_Bank rEQESTOR_CFG bANK_CFG a) (unsafeCoerce coq_Bank rEQESTOR_CFG bANK_CFG b)))
(Eqtype.eq_op Ssrnat.nat_eqType (unsafeCoerce coq_Row rEQESTOR_CFG bANK_CFG a)
(unsafeCoerce coq_Row rEQESTOR_CFG bANK_CFG b))
coq_Request_eqn :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Eqtype.Equality__Coq_axiom
Request_t
coq_Request_eqn rEQESTOR_CFG bANK_CFG x y =
let {b = coq_Request_eqdef rEQESTOR_CFG bANK_CFG x y} in
case b of {
Datatypes.Coq_true -> Bool.ReflectT;
Datatypes.Coq_false -> Bool.ReflectF}
coq_Request_eqMixin :: Bank.Requestor_configuration -> Bank.Bank_configuration ->
Eqtype.Equality__Coq_mixin_of Request_t
coq_Request_eqMixin rEQESTOR_CFG bANK_CFG =
Eqtype.Equality__Mixin (coq_Request_eqdef rEQESTOR_CFG bANK_CFG) (coq_Request_eqn rEQESTOR_CFG bANK_CFG)
coq_Request_eqType :: Bank.Requestor_configuration -> Bank.Bank_configuration -> Eqtype.Equality__Coq_type
coq_Request_eqType rEQESTOR_CFG bANK_CFG =
unsafeCoerce coq_Request_eqMixin rEQESTOR_CFG bANK_CFG
type Requests_t = Datatypes.Coq_list Request_t
module Seq where
import qualified Prelude
import qualified Datatypes
import qualified Eqtype
import qualified Ssrbool
cat :: (Datatypes.Coq_list a1) -> (Datatypes.Coq_list a1) -> Datatypes.Coq_list a1
cat s1 s2 =
case s1 of {
Datatypes.Coq_nil -> s2;
Datatypes.Coq_cons x s1' -> Datatypes.Coq_cons x (cat s1' s2)}
filter :: (Ssrbool.Coq_pred a1) -> (Datatypes.Coq_list a1) -> Datatypes.Coq_list a1
filter a s =
case s of {
Datatypes.Coq_nil -> Datatypes.Coq_nil;
Datatypes.Coq_cons x s' ->
case a x of {
Datatypes.Coq_true -> Datatypes.Coq_cons x (filter a s');
Datatypes.Coq_false -> filter a s'}}
rem :: Eqtype.Equality__Coq_type -> Eqtype.Equality__Coq_sort -> (Datatypes.Coq_list
Eqtype.Equality__Coq_sort) -> Datatypes.Coq_list Eqtype.Equality__Coq_sort
rem t x s =
case s of {
Datatypes.Coq_nil -> s;
Datatypes.Coq_cons y t0 ->
case Eqtype.eq_op t y x of {
Datatypes.Coq_true -> t0;
Datatypes.Coq_false -> Datatypes.Coq_cons y (rem t x t0)}}
module Specif where
import qualified Prelude
type Coq_sig a = a
-- singleton inductive, whose constructor was exist
proj1_sig :: a1 -> a1
proj1_sig e =
e
module Ssrbool where
import qualified Prelude
import qualified Bool
import qualified Datatypes
__ :: any
__ = Prelude.error "Logical or arity value used"
iffP :: Datatypes.Coq_bool -> Bool.Coq_reflect -> Bool.Coq_reflect
iffP _ pb =
let {_evar_0_ = \_ _ _ -> Bool.ReflectT} in
let {_evar_0_0 = \_ _ _ -> Bool.ReflectF} in
case pb of {
Bool.ReflectT -> _evar_0_ __ __ __;
Bool.ReflectF -> _evar_0_0 __ __ __}
idP :: Datatypes.Coq_bool -> Bool.Coq_reflect
idP b1 =
case b1 of {
Datatypes.Coq_true -> Bool.ReflectT;
Datatypes.Coq_false -> Bool.ReflectF}
type Coq_pred t = t -> Datatypes.Coq_bool
type Coq_rel t = t -> Coq_pred t
{-# OPTIONS_GHC -cpp -XMagicHash #-}
{- For Hugs, use the option -F"cpp -P -traditional" -}
module Ssrnat where
import qualified Prelude
import qualified Datatypes
import qualified Nat
import qualified Eqtype
import qualified Ssrbool
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
#else
-- HUGS
import qualified IOExts
#endif
#ifdef __GLASGOW_HASKELL__
unsafeCoerce :: a -> b
unsafeCoerce = GHC.Base.unsafeCoerce#
#else
-- HUGS
unsafeCoerce :: a -> b
unsafeCoerce = IOExts.unsafeCoerce
#endif
eqn :: Prelude.Int -> Prelude.Int -> Datatypes.Coq_bool
eqn m n =
(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
(\_ ->
(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
(\_ -> Datatypes.Coq_true)
(\_ -> Datatypes.Coq_false)
n)
(\m' ->
(\fO fS n -> if n Prelude.== 0 then fO () else fS (n Prelude.- 1))
(\_ -> Datatypes.Coq_false)
(\n' -> eqn m' n')
n)
m
eqnP :: Eqtype.Equality__Coq_axiom Prelude.Int
eqnP n m =
Ssrbool.iffP (eqn n m) (Ssrbool.idP (eqn n m))
nat_eqMixin :: Eqtype.Equality__Coq_mixin_of Prelude.Int
nat_eqMixin =
Eqtype.Equality__Mixin eqn eqnP
nat_eqType :: Eqtype.Equality__Coq_type
nat_eqType =
unsafeCoerce nat_eqMixin
addn_rec :: Prelude.Int -> Prelude.Int -> Prelude.Int
addn_rec =
(Prelude.+)
addn :: Prelude.Int -> Prelude.Int -> Prelude.Int
addn =
addn_rec
subn_rec :: Prelude.Int -> Prelude.Int -> Prelude.Int
subn_rec =
Nat.sub
subn :: Prelude.Int -> Prelude.Int -> Prelude.Int
subn =
subn_rec
leq :: Prelude.Int -> Prelude.Int -> Datatypes.Coq_bool
leq m n =
Eqtype.eq_op nat_eqType (unsafeCoerce subn m n) (unsafeCoerce 0)
module Trace where
import qualified Prelude
import qualified Commands
data Trace_t =
Coq_mkTrace Commands.Commands_t Prelude.Int
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment