case \x of 0 -> 1 -> _ -> ---> if \x = 0 then ->1 else if \x = 1 then ->2 else ->3 case \x of nodeCap@(CNodeCap {}) -> _ -> ---> let nodeCap = \x in if isCNodeCap nodeCap then ->1 else ->2 case \x of root@(CNodeCap {}) -> _ -> ---> let root = \x in if isCNodeCap root then ->1 else ->2 case \x of rt@(CNodeCap {}) -> _ -> ---> let rt = \x in if isCNodeCap rt then ->1 else ->2 case \x of cap@(EndpointCap { capEPCanSend = True }) -> cap@(NotificationCap { capNtfnCanSend = True }) -> cap -> ---> let cap = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else if isNotificationCap cap \ capNtfnCanSend cap then ->2 else ->3 case \x of EndpointCap { \v0\EPCanReceive = True } -> NotificationCap { \v0\NtfnCanReceive = True } -> _ -> ---> let \v0\ = \x in if isEndpointCap \v0\ \ \v0\EPCanReceive \v0 then ->1 else if isNotificationCap \v0\ \ \v0\NtfnCanReceive \v0 then ->2 else ->3 case \x of (_, _, cap@(ThreadCap {capTCBCanWrite = True})) -> (_, _, cap@(CNodeCap {})) -> (_, capIndex, cap@(UntypedCap {})) -> (blocking, capIndex, cap@(ArchObjectCap {})) -> (True, ptr, cap) -> (False, _, _) -> ---> let (blocking, capIndex, cap) = \x in if isThreadCap cap \ capTCBCanWrite cap then ->1 else if isCNodeCap cap then ->2 else if isUntypedCap cap then ->3 else if isArchObjectCap cap then ->4 else if blocking then ->5 else ->6 case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=True}) -> (_, _) -> ---> let (\v0\, cap) = \x in if length (\v0\) > 1 \ isCNodeCap cap \ capCNodeCanModify cap then let index = \v0\ !! 0; bits = \v0\ !! 1; args = drop 2 \v0 in ->1 else if isCNodeCap cap \ capCNodeCanModify cap then ->2 else ->3 case \x of (_, _, cap@(ThreadCap {capTCBCanWrite = True})) -> (_, _, cap@(CNodeCap {capCNodeCanModify = True})) -> (_, capIndex, cap@(UntypedCap {})) -> (blocking, capIndex, cap@(ArchObjectCap {})) -> (True, ptr, cap) -> (False, _, _) -> ---> let (blocking, capIndex, cap) = \x in if isThreadCap cap \ capTCBCanWrite cap then ->1 else if isCNodeCap cap \ capCNodeCanModify cap then ->2 else if isUntypedCap cap then ->3 else if isArchObjectCap cap then ->4 else if blocking then let ptr = capIndex in ->5 else ->6 case \x of (capPtr, cap@(ThreadCap{capTCBCanWrite = True})) -> (_, cap@(CNodeCap {capCNodeCanModify = True})) -> (capIndex, cap@(UntypedCap {})) -> (capIndex, cap@(ArchObjectCap {})) -> (capPtr, cap) -> ---> let (capPtr, cap) = \x; capIndex = capPtr in if isThreadCap cap \ capTCBCanWrite cap then ->1 else if isCNodeCap cap \ capCNodeCanModify cap then ->2 else if isUntypedCap cap then ->3 else if isArchObjectCap cap then ->4 else ->5 case \x of (capPtr, cap@(ThreadCap{capTCBCanWrite = True})) -> (_, cap@(CNodeCap {capCNodeCanModify = True})) -> (_, cap@(UntypedCap {})) -> (capIndex, cap@(ArchObjectCap {})) -> (capPtr, cap) -> ---> let (capPtr, cap) = \x; capIndex = capPtr in if isThreadCap cap \ capTCBCanWrite cap then ->1 else if isCNodeCap cap \ capCNodeCanModify cap then ->2 else if isUntypedCap cap then ->3 else if isArchObjectCap cap then ->4 else ->5 case \x of Just (slot, 0, rights) -> _ -> ---> case \x of Some \v0\ \ let (slot, \v1\, rights) = \v0\ in if \v1\ = 0 then ->1 else ->2 | None \ ->2 case \x of (slot, 0, rights) -> (_, bitsLeft, _) -> ---> let (slot, bitsLeft, rights) = \x in if bitsLeft = 0 then ->1 else ->2 case \x of (index:bits:args, cnode@(CNodeCap {})) -> (_, _) -> ---> let (L, cnode) = \x in if isCNodeCap cnode \ length L > 1 then let index = L !! 0; bits = L !! 1; args = drop 2 L in ->1 else ->2 case \x of (index:bits:args, cnode@(CNodeCap { capCNodeCanModify = True })) -> (_, CNodeCap { capCNodeCanModify = True }) -> (_, _) -> ---> let (L, cnode) = \x in if isCNodeCap cnode \ capCNodeCanModify cnode then if length L > 1 then let index = L !! 0; bits = L !! 1; args = drop 2 L in ->1 else ->2 else ->3 case \x of (YieldToCall, _, thread) -> (call@(ThreadControlCall {}), faultep:replyep:priority:cRoot:cRootData:vRoot:vRootData:buffer:_, target) -> (call@(ExchangeRegistersCall {}), src:save:_, dest) -> (_, _, _) -> ---> let (call, L, \v0\) = \x in if isYieldToCall call then let thread = \v0\ in ->1 else if isThreadControlCall call \ length L > 6 then let target = \v0\; faultep = L !! 0; replyep = L !! 1; priority = L !! 2; cRoot = L !! 3; cRootData = L !! 4; vRoot = L !! 5; vRootData = L !! 6; buffer = L !! 7 in ->2 else if isExchangeRegistersCall call \ length L > 1 then let dest = \v0\; src = L !! 0; save = L !! 1 in ->3 else ->4 case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> (_,_) -> ---> let (call, \v0\) = \x in if isThreadControlCall call \ threadSetCRoot call \ \ \v0 then ->1 else if isThreadControlCall call \ threadSetVRoot call \ \ \v0 then ->2 else ->3 case \x of (call@(ThreadControlCall{threadSetCRoot = True}), False) -> (call@(ThreadControlCall{threadSetVRoot = True}), False) -> _ -> ---> let (call, \v0\) = \x in if isThreadControlCall call \ threadSetCRoot call \ \ \v0 then ->1 else if isThreadControlCall call \ threadSetVRoot call \ \ \v0 then ->2 else ->3 case \x of untypedCap@(UntypedCap {}) -> _ -> ---> let untypedCap = \x in if isUntypedCap untypedCap then ->1 else ->1 case \x of ex2@(UserHandledFault {}) -> ex2 -> ---> let ex2 = \x in if isUserHandledFault ex2 then ->1 else ->2 case \x of 0 -> size -> ---> let size = \x in if size = 0 then ->1 else ->2 case \x of 0 -> ctePtr -> ---> let ctePtr = \x in if ctePtr = 0 then ->1 else ->2 case \x of (first:rest,_) -> ([], 0) -> ([], _) -> ---> let \v0\ = \x in case fst \v0\ of first#rest \ ->1 | [] \ if snd \v0\ = 0 then ->2 else ->3 case \x of Just x@(CNodeData {}) -> _ -> ---> let \v0\ = \x in if \v0\ \ None \ isCNodeData (the \v0\) then let x = the \v0\ in ->1 else ->2 case \x of (Just new, EndpointData 0) -> (Just _, EndpointData _) -> (Just new, AsyncEndpointData 0) -> (Just _, AsyncEndpointData _) -> (Nothing, old@(CNodeData {})) -> (Just new, old@(CNodeData {})) -> (_, old) -> ---> let (\v0\, old) = \x; new = the \v0\; \v1\ = (\v0\ \ None) in if \v1\ \ old = EndpointData 0 then ->1 else if \v1\ \ isEndpointData old then ->2 else if \v1\ \ old = AsyncEndpointData 0 then ->3 else if \v1\ \ isAsyncEndpointData old then ->4 else if (\ \v1\) \ isCNodeData old then ->5 else if \v1\ \ isCNodeData old then ->6 else ->7 case \x of 0 -> slot -> ---> let slot = \x in if slot = 0 then ->1 else ->2 case \x of CTE { cteCap = UntypedCap {} } -> cte@(CTE { cteMDBNode = mdb }) -> ---> let cte = \x in if isUntypedCap (cteCap cte) then ->1 else let mdb = cteMDBNode cte in ->2 case \x of cap@(EndpointCap {}) -> _ -> ---> let cap = \x in if isEndpointCap cap then ->1 else ->2 case \x of (a@UntypedCap {}, b@UntypedCap {}) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (a@FrameCap {}, b@FrameCap {}) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) -> ---> let (a, b) = \x in if isUntypedCap a \ isUntypedCap b then ->1 else if isEndpointCap a \ isEndpointCap b then ->2 else if isNotificationCap a \ isNotificationCap b then ->3 else if isCNodeCap a \ isCNodeCap b then ->4 else if isThreadCap a \ isThreadCap b then ->5 else if isFrameCap a \ isFrameCap b then ->6 else if isArchObjectCap a \ isArchObjectCap b then let a = capCap a; b = capCap b in ->7 else ->8 case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ThreadCap {capTCBCanWrite=True}) -> cap@(CNodeCap {capCNodeCanModify=True}) -> cap@(UntypedCap {}) -> cap@(ArchObjectCap {}) -> _ -> ---> let cap = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else if isNotificationCap cap \ capNtfnCanSend cap then ->2 else if isThreadCap cap \ capTCBCanWrite cap then ->3 else if isCNodeCap cap \ capCNodeCanModify cap then ->4 else if isUntypedCap cap then ->5 else if isArchObjectCap cap then ->6 else ->7 case \x of 0 -> 1 -> 2 -> _ -> ---> let \v0\ = \x in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else ->4 case \x of (CTE a@(UntypedCap {}) _, CTE b _) -> (CTE a mdbA, CTE b mdbB) -> ---> let (\v0\, \v1\) = \x in case \v0\ of CTE a mdbA \ ( case \v1\ of CTE b mdbB \ ( if isUntypedCap a then ->1 else ->2 )) case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> (NotificationCap {}) -> _ -> ---> let \v0\ = \x in if isEndpointCap \v0\ \ capEPBadge \v0\ = 0 then ->1 else if isNotificationCap \v0\ \ capNtfnBadge \v0\ = 0 then ->2 else if isEndpointCap \v0 then ->3 else if isNotificationCap \v0 then ->4 else ->5 case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, True) -> (ThreadCap { capTCBPtr = tcb }, True, True) -> (CNodeCap { capCNodePtr = cn }, True, False) -> (Zombie { zombieObject = Left (cn, n+1) }, _, False) -> (ThreadCap { capTCBPtr = tcb }, True, False) -> (Zombie { zombieObject = Right tcb }, True, False) -> (Zombie { zombieObject = Left (cn, n+1) }, _, True) -> (Zombie { zombieObject = Left (_, 0) }, True, _) -> (Zombie { zombieObject = Right tcb }, True, True) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ \ \v1 then let ptr = capEPPtr \v0 in ->1 else if isNotificationCap \v0\ \ \v1 then let ptr = capNtfnPtr \v0 in ->2 else if isCNodeCap \v0\ \ \v1\ \ \v2 then let cap = \v0 in ->3 else if isThreadCap \v0\ \ \v1\ \ \v2 then let tcb = capTCBPtr \v0 in ->4 else if isCNodeCap \v0\ \ \v1\ \ (\ \v2\) then let cn = capCNodePtr \v0 in ->5 else if isZombie \v0\ \ (\ \v2\) \ (\cn n. zombieObject \v0\ = Left (cn, n + 1)) then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1 in ->6 else if isThreadCap \v0\ \ \v1\ \ (\ \v2\) then let tcb = capTCBPtr \v0 in ->7 else if isZombie \v0\ \ \v1\ \ (\ \v2\) \ isRight (zombieObject \v0\) then let tcb = theRight (zombieObject \v0\) in ->8 else if isZombie \v0\ \ \v2\ \ (\cn n. zombieObject \v0\ = Left (cn, n + 1)) then let (cn, \v3\) = theLeft (zombieObject \v0\); n = \v3\ - 1 in ->9 else if isZombie \v0\ \ \v1\ \ (\\v3\. zombieObject \v0\ = Left (\v3\, 0)) then ->10 else if isZombie \v0\ \ isRight (zombieObject \v0\) \ \v1\ \ \v2 then let tcb = theRight (zombieObject \v0\) in ->11 else if isArchObjectCap \v0 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->12 else if isFrameCap \v0 then ->13 else if isNullCap \v0 then ->14 else if isZombie \v0\ \ (\ \v1\) then ->15 else ->16 case \x of (new, cap@(EndpointCap {})) -> (new, cap@(NotificationCap {})) -> (w, cap@(CNodeCap {})) -> (w, ArchObjectCap { capCap = aoCap }) -> (_, cap) -> ---> let (new, cap) = \x; w = new in if isEndpointCap cap then ->1 else if isNotificationCap cap then ->2 else if isCNodeCap cap then ->3 else if isArchObjectCap cap then let aoCap = capCap cap in ->4 else ->5 case \x of cap@(EndpointCap { capEPCanSend = True }) -> _ -> ---> let cap = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else ->2 case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, _, False) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, _, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ \ \v1 then let ptr = capEPPtr \v0 in ->1 else if isNotificationCap \v0\ \ \v1 then let ptr = capNtfnPtr \v0 in ->2 else if isCNodeCap \v0\ \ \v1 then let cap = \v0\; exposed = \v2 in ->3 else if isThreadCap \v0\ \ \v1 then let tcb = capTCBPtr \v0\; exposed = \v2 in ->4 else if isZombie \v0\ \ (\ \v2\) \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->5 else if isZombie \v0\ \ \v2\ \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->6 else if isZombie \v0\ \ capNumber \v0\ = 0 then ->7 else if isArchObjectCap \v0 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->8 else if isFrameCap \v0 then ->9 else if isNullCap \v0 then ->10 else if isZombie \v0\ \ (\ \v1\) then ->11 else ->12 case \x of (index:bits:args, cap@(CNodeCap {capCNodeCanModify=True})) -> (_, CNodeCap {capCNodeCanModify=False}) -> (_, _) -> ---> let (\v0\, cap) = \x in if length (\v0\) > 1 \ isCNodeCap cap \ capCNodeCanModify cap then let index = \v0\ !! 0; bits = \v0\ !! 1; args = drop 2 \v0 in ->1 else if isCNodeCap cap \ (\ capCNodeCanModify cap) then ->2 else ->3 case \x of 32 -> 64 -> _ -> ---> if \x = 32 then ->1 else if \x = 64 then ->2 else ->3 case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@(FrameCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) -> ---> let c = \x in if isNullCap c then ->1 else if isUntypedCap c then ->2 else if isEndpointCap c then ->3 else if isNotificationCap c then ->4 else if isCNodeCap c then ->5 else if isThreadCap c then ->6 else if isFrameCap c then ->7 else if isArchObjectCap c then let aoCap = capCap c in ->8 else (* assuming Zombie *) ->9 case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) -> ---> let (src, new) = \x in if (isEndpointCap src \ isEndpointCap new) then ->1 else if (isNotificationCap src \ isNotificationCap new) then ->2 else ->3 case \x of c2@(Zombie { capCTEPtr = ptr2 }) -> _ -> ---> let c2 = \x; ptr2 = capCTEPtr c2 in if isZombie c2 then ->1 else ->2 case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ \ \v1 then let ptr = capEPPtr \v0 in ->1 else if isNotificationCap \v0\ \ \v1 then let ptr = capNtfnPtr \v0 in ->2 else if isCNodeCap \v0\ \ \v1 then let cap = \v0\; exposed = \v2 in ->3 else if isThreadCap \v0\ \ \v1 then let tcb = capTCBPtr \v0\; exposed = \v2 in ->4 else if isZombie \v0\ \ \v1\ \ (\ \v2\) \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->5 else if isZombie \v0\ \ \v1\ \ \v2\ \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1; c = \v0 in ->6 else if isZombie \v0\ \ \v1\ \ capNumber \v0\ = 0 then ->7 else if isArchObjectCap \v0 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->8 else if isFrameCap \v0 then ->9 else if isNullCap \v0 then ->10 else if isZombie \v0\ \ (\ \v1\) then ->11 else ->12 case \x of (src@EndpointCap {}, new@EndpointCap {}) -> (src@NotificationCap {}, new@NotificationCap {}) -> (_, _) -> ---> let (src,new) = \x in if isEndpointCap src & isEndpointCap new then ->1 else if isNotificationCap src & isNotificationCap new then ->2 else ->3 case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap {} -> NotificationCap {} -> _ -> ---> if isEndpointCap \x \ capEPBadge \x = 0 then ->1 else if isNotificationCap \x \ capNtfnBadge \x = 0 then ->2 else if isEndpointCap \x then ->3 else if isNotificationCap \x then ->4 else ->5 case \x of (_, cap@(EndpointCap {capEPCanSend=True})) -> (_, cap@(NotificationCap {capNtfnCanSend=True})) -> (sl, cap@(ThreadCap {capTCBCanWrite=True})) -> (_, cap@(CNodeCap {capCNodeCanModify=True})) -> (slot, cap@(UntypedCap {})) -> (slot, cap@(ArchObjectCap {})) -> (_, _) -> ---> let (slot, cap) = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else if isNotificationCap cap \ capNtfnCanSend cap then ->2 else if isThreadCap cap \ capTCBCanWrite cap then let sl = slot in ->3 else if isCNodeCap cap \ capCNodeCanModify cap then ->4 else if isUntypedCap cap then ->5 else if isArchObjectCap cap then ->6 else ->7 case \x of EndpointCap { capEPBadge = 0 } -> NotificationCap { capNtfnBadge = 0 } -> EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ -> ---> if isEndpointCap \x & capEPBadge \x = 0 then ->1 else if isNotificationCap \x & capNtfnBadge \x = 0 then ->2 else if isEndpointCap \x then let badge = capEPBadge \x in ->3 else if isNotificationCap \x then let badge = capNtfnBadge \x in ->4 else ->5 case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (a@FrameCap {}, b@FrameCap {}) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) -> ---> let (a,b) = \x in if b = NullCap then ->1 else if isUntypedCap a then ->2 else if isEndpointCap a & isEndpointCap b then ->3 else if isNotificationCap a & isNotificationCap b then ->4 else if isCNodeCap a & isCNodeCap b then ->5 else if isThreadCap a & isThreadCap b then ->6 else if isFrameCap a & isFrameCap b then ->7 else if isArchObjectCap a & isArchObjectCap b then let a = capCap a; b = capCap b in ->8 else ->9 case \x of EndpointCap { capEPBadge = badge } | badge /= 0 -> NotificationCap { capNtfnBadge = badge } | badge /= 0 -> _ -> ---> if isEndpointCap \x & capEPBadge \x ~= 0 then let badge = capEPBadge \x in ->1 else if isNotificationCap \x & capNtfnBadge \x ~= 0 then let badge = capNtfnBadge \x in ->2 else ->3 case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True, True) -> (Zombie { capNumber = 0 }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (FrameCap {}, _, _) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ \ \v1 then let ptr = capEPPtr \v0 in ->1 else if isNotificationCap \v0\ \ \v1 then let ptr = capNtfnPtr \v0 in ->2 else if isCNodeCap \v0\ \ \v1 then let cap = \v0\; exposed = \v2 in ->3 else if isThreadCap \v0\ \ \v1 then let tcb = capTCBPtr \v0\; exposed = \v2 in ->4 else if isZombie \v0\ \ \v1\ \ (\ \v2\) \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->5 else if isZombie \v0\ \ \v1\ \ \v2\ \ capNumber \v0\ \ 0 then let z = \v0\; ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1; c = \v0 in ->6 else if isZombie \v0\ \ \v1\ \ capNumber \v0\ = 0 then ->7 else if isArchObjectCap \v0 then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->8 else if isFrameCap \v0 then ->9 else if isNullCap \v0 then ->10 else if isZombie \v0\ \ (\ \v1\) then ->11 else ->12 case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 6 -> (_, _) | label > 6 -> _ -> ---> let (\v0\, \v1\) = \x in if length \v0\ >= 2 & length \v1\ >= 1 & label < 4 then let srcIndex = \v0\ !! 0; srcDepth = \v0\ !! 1; args = drop 2 \v0\; srcRootCap = \v1\ !! 0 in ->1 else if label = 4 then ->2 else if label = 5 then ->3 else if length \v0\ >= 6 & length \v1\ >= 2 & label = 6 then let pivotNewData = \v0\ !! 0; pivotIndex = \v0\ !! 1; pivotDepth = \v0\ !! 2; srcNewData = \v0\ !! 3; srcIndex = \v0\ !! 4; srcDepth = \v0\ !! 5; pivotRootCap = \v1\ !! 0; srcRootCap = \v1\ !! 1 in ->4 else if label > 6 then ->5 else ->6 case \x of Zombie {} -> cap@(UntypedCap {}) -> ArchObjectCap cap -> cap -> ---> let cap = \x in case cap of Zombie \v0\ \v1\ \v2\ \ ->1 | UntypedCap \v0\ \v1\ \ ->2 | ArchObjectCap cap \ ->3 | _ \ ->4 case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> _ -> ---> let \v0\ = \x in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else if \v0\ = 3 then ->4 else if \v0\ = 4 then ->5 else if \v0\ = 5 then ->6 else if \v0\ = 6 then ->7 else if \v0\ = 7 then ->8 else ->9 case \x of MI { msgExtraCaps = 0 } -> MI { msgExtraCaps = count } -> ---> let \v0\ = \x in if msgExtraCaps \v0\ = 0 then ->1 else let count = msgExtraCaps \v0\ in ->2 case \x of c@PageTableCap { capPTMappedAddress = Just _ } -> PageTableCap { capPTMappedAddress = Nothing } -> c@PageDirectoryCap { capPDMappedASID = Just _ } -> PageDirectoryCap { capPDMappedASID = Nothing } -> c@PageCap {} -> c@ASIDControlCap -> c@ASIDPoolCap {} -> ---> let c = \x in case c of PageTableCap \v0\ \v1\ \ if \v1\ = None then ->2 else ->1 | PageDirectoryCap \v0\ \v1\ \ if \v1\ = None then ->4 else ->3 | PageCap \v0\ \v1\ \v2\ \v3\ \ ->5 | ASIDControlCap \ ->6 | ASIDPoolCap \v0\ \v1\ \ ->7 case \x of c@(PageCap {}) -> c -> ---> let c = \x in if isPageCap c then ->1 else ->2 case \x of (a@PageCap {}, b@PageCap {}) -> (a@PageTableCap {}, b@PageTableCap {}) -> (a@PageDirectoryCap {}, b@PageDirectoryCap {}) -> (ASIDControlCap, ASIDControlCap) -> (a@ASIDPoolCap {}, b@ASIDPoolCap {}) -> (_, _) -> ---> let (a, b) = \x in if (isPageCap a & isPageCap b) then ->1 else if (isPageTableCap a & isPageTableCap b) then ->2 else if (isPageDirectoryCap a & isPageDirectoryCap b) then ->3 else if (isASIDControlCap a & isASIDControlCap b) then ->4 else if (isASIDPoolCap a & isASIDPoolCap b) then ->5 else ->6 case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.SectionObject -> Arch.Types.SuperSectionObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> ---> case \x of Arch.Types.APIObjectType \v0\ \ ->1 | Arch.Types.SmallPageObject \ ->2 | Arch.Types.LargePageObject \ ->3 | Arch.Types.SectionObject \ ->4 | Arch.Types.SuperSectionObject \ ->5 | Arch.Types.PageTableObject \ ->6 | Arch.Types.PageDirectoryObject \ ->7 case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 7 -> (_, _) | label > 7 -> _ -> ---> let (\v0\, \v1\) = \x in if length \v0\ >= 2 & length \v1\ >= 1 & label < 4 then let srcIndex = \v0\ !! 0; srcDepth = \v0\ !! 1; args = drop 2 \v0\; srcRootCap = \v1\ !! 0 in ->1 else if label = 4 then ->2 else if label = 5 then ->3 else if label = 6 then ->4 else if length \v0\ >= 6 & length \v1\ >= 2 & label = 7 then let pivotNewData = \v0\ !! 0; pivotIndex = \v0\ !! 1; pivotDepth = \v0\ !! 2; srcNewData = \v0\ !! 3; srcIndex = \v0\ !! 4; srcDepth = \v0\ !! 5; pivotRootCap = \v1\ !! 0; srcRootCap = \v1\ !! 1 in ->5 else if label > 7 then ->6 else ->7 case \x of IdleEP | blocking -> SendEP queue | blocking -> IdleEP -> SendEP _ -> RecvEP (dest:queue) -> RecvEP [] -> ---> case \x of IdleEP \ if blocking then ->1 else ->3 | SendEP queue \ if blocking then ->2 else ->4 | RecvEP \v0\ \ (case \v0\ of dest # queue \ ->5 | [] \ ->6 ) case \x of Zombie {} -> cap@(UntypedCap {}) -> ReplyCap {} -> ArchObjectCap cap -> cap -> ---> let cap = \x in case cap of Zombie \v0\ \v1\ \v2\ \ ->1 | UntypedCap \v0\ \v1\ \ ->2 | ReplyCap \v0\ \v1\ \ ->3 | ArchObjectCap cap \ ->4 | _ \ ->5 case \x of (EndpointCap { capEPPtr = ptr }, True, _) -> (NotificationCap { capNtfnPtr = ptr }, True, _) -> (cap@(CNodeCap {}), True, exposed) -> (ThreadCap { capTCBPtr = tcb }, True, exposed) -> (Zombie { capCTEPtr = ptr, capNumber = n+1 }, True, False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True, True) -> (Zombie { capNumber = 0 }, True, _) -> (IRQHandlerCap { capIRQ = irq }, True, _) -> (ArchObjectCap { capCap = cap }, final, exposed) -> (NullCap, _, _) -> (Zombie {}, False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ \ \v1\ then let ptr = capEPPtr \v0 in ->1 else if isNotificationCap \v0\ \ \v1\ then let ptr = capNtfnPtr \v0 in ->2 else if isCNodeCap \v0\ \ \v1\ then let cap = \v0\; exposed = \v2\ in ->3 else if isThreadCap \v0\ \ \v1\ then let tcb = capTCBPtr \v0\; exposed = \v2\ in ->4 else if isZombie \v0\ \ \v1\ \ (\ \v2\) \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->5 else if isZombie \v0\ \ \v1\ \ \v2\ \ capNumber \v0\ \ 0 then let z = \v0\; ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1; c = \v0\ in ->6 else if isZombie \v0\ \ \v1\ \ capNumber \v0\ = 0 then ->7 else if isIRQHandlerCap \v0\ \ \v1\ then let irq = capIRQ \v0\ in ->8 else if isArchObjectCap \v0\ then let (cap, final, exposed) = (capCap \v0\, \v1\, \v2\) in ->9 else if isNullCap \v0\ then ->10 else if isZombie \v0\ \ (\ \v1\) then ->11 else ->12 case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> (a@EndpointCap {}, b@EndpointCap {}) -> (a@NotificationCap {}, b@NotificationCap {}) -> (a@CNodeCap {}, b@CNodeCap {}) -> (a@ThreadCap {}, b@ThreadCap {}) -> (IRQControlCap, IRQControlCap) -> (IRQHandlerCap a, IRQHandlerCap b) -> (ArchObjectCap a, ArchObjectCap b) -> (_, _) -> --->let (a,b) = \x in if b = NullCap then ->1 else if isUntypedCap a then ->2 else if isEndpointCap a & isEndpointCap b then ->3 else if isNotificationCap a & isNotificationCap b then ->4 else if isCNodeCap a & isCNodeCap b then ->5 else if isThreadCap a & isThreadCap b then ->6 else if a = IRQControlCap & b = IRQControlCap then ->7 else if isIRQHandlerCap a & isIRQHandlerCap b then let a = capIRQ a; b = capIRQ b in ->8 else if isArchObjectCap a & isArchObjectCap b then let a = capCap a; b = capCap b in ->9 else ->10 case \x of (preserve, new, cap@(EndpointCap {})) -> (preserve, new, cap@(NotificationCap {})) -> (_, w, cap@(CNodeCap {})) -> (p, w, ArchObjectCap { capCap = aoCap }) -> (_, _, cap) -> --->let (\v0\, \v1\, \v2\ ) = \x in if isEndpointCap \v2\ then let preserve = \v0\; new = \v1\; cap = \v2\ in ->1 else if isNotificationCap \v2\ then let preserve = \v0\; new = \v1\; cap = \v2\ in ->2 else if isCNodeCap \v2\ then let w = \v1\; cap = \v2\ in ->3 else if isArchObjectCap \v2\ then let p = \v0\; w = \v1\; aoCap = capCap \v2\ in ->4 else let cap = \v2\ in ->5 case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> ArchObjectCap {capCap = aoCap} -> c@(Zombie {}) -> --->let c = \x in if isNullCap c then ->1 else if isUntypedCap c then ->2 else if isEndpointCap c then ->3 else if isNotificationCap c then ->4 else if isReplyCap c then ->5 else if isCNodeCap c then ->6 else if isThreadCap c then ->7 else if isIRQControlCap c then ->8 else if isIRQHandlerCap c then ->9 else if isArchObjectCap c then let aoCap = capCap c in ->10 else (* assuming Zombie *) ->11 case \x of 0 -> 1 -> 2 -> 3 -> 4 -> 5 -> 6 -> 7 -> 8 -> 9 -> _ -> --->let \v0\ = \x in if \v0\ = 0 then ->1 else if \v0\ = 1 then ->2 else if \v0\ = 2 then ->3 else if \v0\ = 3 then ->4 else if \v0\ = 4 then ->5 else if \v0\ = 5 then ->6 else if \v0\ = 6 then ->7 else if \v0\ = 7 then ->8 else if \v0\ = 8 then ->9 else if \v0\ = 9 then ->10 else ->11 case \x of ArchObjectCap (pageCap@PageCap {}) -> _ -> ---> let \v0\ = \x in if isArchObjectCap \v0\ \ isPageCap (capCap \v0\) then let pageCap = capCap \v0\ in ->1 else ->2 case \x of ArchObjectCap (frameCap@PageCap {}) -> _ -> ---> let \v0\ = \x in if isArchObjectCap \v0\ \ isPageCap (capCap \v0\) then let frameCap = capCap \v0\ in ->1 else ->2 case \x of ((Zombie { capCTEPtr = ptr, capNumber = n+1 }), False) -> (z@(Zombie { capCTEPtr = ptr, capNumber = n+1 }), True) -> (_, _) -> ---> let (\v0\, \v1\) = \x in if isZombie \v0\ \ (\ \v1\) \ capNumber \v0\ \ 0 then let ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->1 else if isZombie \v0\ \ \v1\ \ capNumber \v0\ \ 0 then let z = \v0\; ptr = capCTEPtr \v0\; n = capNumber \v0\ - 1 in ->2 else ->3 case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedASID = Just _ }) -> (PageDirectoryCap { capPDMappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> ---> let c = \x in if isPageTableCap c \ capPTMappedAddress c \ None then ->1 else if isPageTableCap c \ capPTMappedAddress c = None then ->2 else if isPageDirectoryCap c \ capPDMappedASID c \ None then ->3 else if isPageDirectoryCap c \ capPDMappedASID c = None then ->4 else if isPageCap c then ->5 else if isASIDControlCap c then ->6 else if isASIDPoolCap c then ->7 else undefined case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> (_, _) -> ---> let (a, b) = \x in if isPageCap a \ isPageCap b then ->1 else if isPageTableCap a \ isPageTableCap b then ->2 else if isPageDirectoryCap a \ isPageDirectoryCap b then ->3 else if isASIDControlCap a \ isASIDControlCap b then ->4 else if isASIDPoolCap a \ isASIDPoolCap b then ->5 else ->6 case \x of ArchObjectCap (frame@PageCap {}) -> _ -> ---> let \v0\ = \x in if isArchObjectCap \v0\ \ isPageCap (capCap \v0\) then let frame = capCap \v0\ in ->1 else ->2 case \x of ArchObjectCap (PageDirectoryCap { capPDMappedASID = Just _, capPDBasePtr = cur_pd }) | cur_pd == pd -> _ -> ---> let \v0\ = \x in if isArchObjectCap \v0\ \ isPageDirectoryCap (capCap \v0\) \ capPDMappedASID (capCap \v0\) \ None \ capPDBasePtr (capCap \v0\) = pd then let cur_pd = pd in ->1 else ->2 case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in if \v0\ = 0 then if length \v1\ > 1 \ length \v2\ > 0 then let vaddr = \v1\ !! 0; attr = \v1\ !! 1; pdCap = fst (\v2\ !! 0) in ->1 else ->2 else ->3 case \x of (0, vaddr:rightsMask:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, rightsMask:attr:_, _) -> (1, _, _) -> (2, _, _) -> (3, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in if \v0\ = 0 then if length \v1\ > 2 \ length \v2\ > 0 then let vaddr = \v1\ !! 0; rightsMask = \v1\ !! 1; attr = \v1\ !! 2; pdCap = fst (\v2\ !! 0) in ->1 else ->2 else if \v0\ = 1 then if length \v1\ > 1 then let rightsMask = \v1\ !! 0; attr = \v1\ !! 1 in ->3 else ->4 else if \v0\ = 2 then ->5 else if \v0\ = 3 then ->6 else ->7 case \x of (0, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (0, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in if \v0\ = 0 then if length \v1\ > 1 \ length \v2\ > 1 then let index = \v1\ !! 0; depth = \v1\ !! 1; (untyped, parentSlot) = \v2\ !! 0; croot = fst (\v2\ !! 1) in ->1 else ->2 else ->3 case \x of (0, (pdCap,pdCapSlot):_) -> (0, _) -> _ -> ---> let (\v0\, \v1\) = \x in if \v0\ = 0 then if length \v1\ > 0 then let (pdCap, pdCapSlot) = \v1\ !! 0 in ->1 else ->2 else ->3 case \x of (PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> ---> let cap = \x in if isPageDirectoryCap cap then ->1 else if isPageTableCap cap then ->2 else if isPageCap cap then ->3 else if isASIDControlCap cap then ->4 else if isASIDPoolCap cap then ->5 else undefined case \x of ((index:bits:args), cap@(CNodeCap {capCNodeCanModify=True})) -> (_, (CNodeCap {capCNodeCanModify=True})) -> (_, _) -> ---> let (\v0\, cap) = \x in if isCNodeCap cap \ capCNodeCanModify cap then (case \v0\ of (index # bits # args) \ ->1 | _ \ ->2 ) else ->3 case \x of ((src@EndpointCap {}), (new@EndpointCap {})) -> ((src@NotificationCap {}), (new@NotificationCap {})) -> (_, _) -> ---> let (src, new) = \x in if isEndpointCap src \ isEndpointCap new then ->1 else if isNotificationCap src \ isNotificationCap new then ->2 else ->3 case \x of (CTE { cteCap = UntypedCap {} }) -> cte@(CTE { cteMDBNode = mdb }) -> ---> let \v0\ = \x in if isUntypedCap (cteCap \v0\) then ->1 else let cte = \v0\; mdb = cteMDBNode cte in ->2 case \x of 0 | length msg >= length syscallMessage -> _ -> ---> if \x = 0 \ length msg \ length syscallMessage then ->1 else ->2 case \x of 0 | length msg >= length exceptionMessage -> _ -> ---> if \x = 0 \ length msg \ length exceptionMessage then ->1 else ->2 case \x of (0,irqW:index:depth:_,cnode:_) -> (0,_,_) -> (1,_,_) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in if \v0\ = 0 then if length \v1\ > 2 \ length \v2\ > 0 then let irqW = \v1\ !! 0; index = \v1\ !! 1; depth = \v1\ !! 2; cnode = \v2\ !! 0 in ->1 else ->2 else if \v0\ = 1 then ->3 else ->4 case \x of (0,_) -> (1,(cap,slot):_) -> (1,_) -> (2,_) -> _ -> ---> let (\v0\, \v1\) = \x in if \v0\ = 0 then ->1 else if \v0\ = 1 then if length \v1\ > 0 then let (cap, slot) = \v1\ !! 0 in ->2 else ->3 else if \v0\ = 2 then ->4 else ->5 case \x of (Zombie {}) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in if isZombie cap then ->1 else if isUntypedCap cap then ->2 else if isReplyCap cap then ->3 else if isArchObjectCap cap then let cap = capCap cap in ->4 else ->5 case \x of ((EndpointCap { capEPPtr = ptr }), True) -> ((NotificationCap { capNtfnPtr = ptr }), True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True) -> ((ThreadCap { capTCBPtr = tcb}), True) -> (z@(Zombie {}), True) -> ((ArchObjectCap { capCap = cap }), final) -> ((IRQHandlerCap { capIRQ = irq }), True) -> (NullCap, _) -> ((Zombie {}), False) -> (_, _) -> ---> let (\v0\, \v1\) = \x in if isEndpointCap \v0\ \ \v1\ then let ptr = capEPPtr \v0\ in ->1 else if isNotificationCap \v0\ \ \v1\ then let ptr = capNtfnPtr \v0\ in ->2 else if isCNodeCap \v0\ \ \v1\ then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ in ->3 else if isThreadCap \v0\ \ \v1\ then let tcb = capTCBPtr \v0\ in ->4 else if isZombie \v0\ \ \v1\ then let z = \v0\ in ->5 else if isArchObjectCap \v0\ then let cap = capCap \v0\; final = \v1\ in ->6 else if isIRQHandlerCap \v0\ \ \v1\ then let irq = capIRQ \v0\ in ->7 else if isNullCap \v0\ then ->8 else if isZombie \v0\ \ \ \v1\ then ->9 else ->10 case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> (IRQControlCap, IRQControlCap) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in if isNullCap b then ->1 else if isUntypedCap a then ->2 else if isEndpointCap a \ isEndpointCap b then ->3 else if isNotificationCap a \ isNotificationCap b then ->4 else if isCNodeCap a \ isCNodeCap b then ->5 else if isThreadCap a \ isThreadCap b then ->6 else if isIRQControlCap a \ isIRQControlCap b then ->7 else if isIRQHandlerCap a \ isIRQHandlerCap b then (case (a, b) of (IRQHandlerCap a, IRQHandlerCap b) \ ->8 ) else if isArchObjectCap a \ isArchObjectCap b then (case (a, b) of (ArchObjectCap a, ArchObjectCap b) \ ->9 ) else ->10 case \x of (preserve, new, cap@(EndpointCap {})) -> (preserve, new, cap@(NotificationCap {})) -> (_, w, cap@(CNodeCap {})) -> (p, w, (ArchObjectCap { capCap = aoCap })) -> (_, _, cap) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v2\ then let preserve = \v0\; new = \v1\; cap = \v2\ in ->1 else if isNotificationCap \v2\ then let preserve = \v0\; new = \v1\; cap = \v2\ in ->2 else if isCNodeCap \v2\ then let w = \v1\; cap = \v2\ in ->3 else if isArchObjectCap \v2\ then let p = \v0\; w = \v1\; aoCap = capCap \v2\ in ->4 else let cap = \v2\ in ->5 case \x of NullCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> (ArchObjectCap {capCap = aoCap}) -> c@(Zombie {}) -> ---> let c = \x; aoCap = capCap \x in if isNullCap c then ->1 else if isUntypedCap c then ->2 else if isEndpointCap c then ->3 else if isNotificationCap c then ->4 else if isReplyCap c then ->5 else if isCNodeCap c then ->6 else if isThreadCap c then ->7 else if isIRQControlCap c then ->8 else if isIRQHandlerCap c then ->9 else if isArchObjectCap c then ->10 else if isZombie c then ->11 else undefined case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {capTCBCanWrite=True}) -> cap@(CNodeCap {capCNodeCanModify=True}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ -> ---> let cap = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else if isNotificationCap cap \ capNtfnCanSend cap then ->2 else if isReplyCap cap \ \ capReplyMaster cap then ->3 else if isThreadCap cap \ capTCBCanWrite cap then ->4 else if isCNodeCap cap \ capCNodeCanModify cap then ->5 else if isUntypedCap cap then ->6 else if isIRQControlCap cap then ->7 else if isIRQHandlerCap cap then let irq = capIRQ cap in ->8 else if isArchObjectCap cap then let cap = capCap cap in ->9 else ->10 case \x of (EndpointCap { capEPPtr = p1 }, Just p2, _) | p1 == p2 -> (_, _, destSlot:slots') -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ \ \v1\ \ None \ capEPPtr \v0\ = the \v1\ then let p1 = capEPPtr \v0\; p2 = p1 in ->1 else (case \v2\ of destSlot # slots' \ ->2 | _ \ ->3 ) case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> ((IRQHandlerCap { capIRQ = irq }), True, _) -> (NullCap, _, _) -> ((Zombie {}), False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ then let ptr = capEPPtr \v0\; final = \v1\ in ->1 else if isNotificationCap \v0\ then let ptr = capNtfnPtr \v0\; final = \v1\ in ->2 else if isReplyCap \v0\ then ->3 else if \v2\ then ->4 else if isCNodeCap \v0\ \ \v1\ then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ in ->5 else if isThreadCap \v0\ \ \v1\ then let tcb = capTCBPtr \v0\ in ->6 else if isZombie \v0\ \ \v1\ then let z = \v0\ in ->7 else if isArchObjectCap \v0\ then let cap = capCap \v0\; final = \v1\ in ->8 else if isIRQHandlerCap \v0\ \ \v1\ then let irq = capIRQ \v0\ in ->9 else if isNullCap \v0\ then ->10 else if isZombie \v0\ \ \ \v1\ then ->11 else ->12 case \x of (cap@PageCap { capVPIsDevice = isDevice }) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> ---> let cap = \x in if isPageCap cap then let isDevice = capVPIsDevice cap in ->1 else if isPageTableCap cap then let ptr = capPTBasePtr cap in ->2 else if isPageDirectoryCap cap then let ptr = capPDBasePtr cap in ->3 else if isASIDControlCap cap then ->4 else if isASIDPoolCap cap then let base = capASIDBase cap; ptr = capASIDPool cap in ->5 else undefined case \x of ArchObjectCap (frame@PageCap {capVPIsDevice = False}) -> _ -> ---> let cap = \x in if isPageCap cap \ \ capVPIsDevice cap then ->1 else ->2 case \x of (srcIndex:srcDepth:args, srcRootCap:_) | label < 4 -> (_, _) | label == 4 -> (_, _) | label == 5 -> (_, _) | label == 6 -> (_, _) | label == 7 -> (pivotNewData:pivotIndex:pivotDepth:srcNewData:srcIndex:srcDepth:_, pivotRootCap:srcRootCap:_) | label == 8 -> (_, _) | label > 8 -> _ -> ---> let (\v0\, \v1\) = \x in case (if label < 4 then 1 else if label = 4 then 2 else if label = 5 then 3 else if label = 6 then 4 else if label = 7 then 5 else if label = 8 then 6 else if label > 8 then 7 else 0, \v0\, \v1\) of (Suc 0, srcIndex # srcDepth # args, srcRootCap # _) \ ->1 | (Suc (Suc 0), _, _) \ ->2 | (Suc (Suc (Suc 0)), _, _) \ ->3 | (Suc (Suc (Suc (Suc 0))), _, _) \ ->4 | (Suc (Suc (Suc (Suc (Suc 0)))), _, _) \ ->5 | (Suc (Suc (Suc (Suc (Suc (Suc 0))))), pivotNewData#pivotIndex#pivotDepth#srcNewData#srcIndex#srcDepth#_, pivotRootCap#srcRootCap#_) \ ->6 | (Suc (Suc (Suc (Suc (Suc (Suc (Suc 0)))))), _, _) \ ->7 | _ \ ->8 case \x of c2@(Zombie { capZombiePtr = ptr2 }) -> _ -> ---> let \v0\ = \x in if isZombie \v0\ then let c2 = \v0\; ptr2 = capZombiePtr c2 in ->1 else ->2 case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n+1 }), True) -> (_, _) -> ---> let (\v0\, \v1\) = \x in if isZombie \v0\ \ capZombieNumber \v0\ = 0 then ->1 else if isZombie \v0\ \ \ \v1\ then let ptr = capZombiePtr \v0\ in ->2 else if isZombie \v0\ \ \v1\ then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z - 1 in ->3 else ->4 case \x of NullCap -> (CNodeCap {}) -> (ThreadCap {}) -> (Zombie { capZombiePtr = ptr, capZombieType = tp, capZombieNumber = n}) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in if isNullCap cap then ->1 else if isCNodeCap cap then ->2 else if isThreadCap cap then ->3 else if isZombie cap then let ptr = capZombiePtr cap; tp = capZombieType cap; n = capZombieNumber cap in ->4 else if isEndpointCap cap then let ep = capEPPtr cap; b = capEPBadge cap in ->5 else if isArchObjectCap cap then let cap = capCap cap in ->6 else ->7 case \x of (_, NullCap) -> (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in if isNullCap b then ->1 else if isUntypedCap a then ->2 else if isEndpointCap a \ isEndpointCap b then ->3 else if isNotificationCap a \ isNotificationCap b then ->4 else if isCNodeCap a \ isCNodeCap b then ->5 else if isThreadCap a \ isThreadCap b then ->6 else if isIRQControlCap a \ isIRQControlCap b then ->7 else if isIRQControlCap a \ isIRQHandlerCap b then ->8 else if isIRQHandlerCap a \ isIRQHandlerCap b then (case (a, b) of (IRQHandlerCap a, IRQHandlerCap b) \ ->9 ) else if isArchObjectCap a \ isArchObjectCap b then (case (a, b) of (ArchObjectCap a, ArchObjectCap b) \ ->10 ) else ->11 case \x of (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> ((a@ReplyCap {}), (b@ReplyCap {})) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in if isUntypedCap a then ->1 else if isEndpointCap a \ isEndpointCap b then ->2 else if isNotificationCap a \ isNotificationCap b then ->3 else if isCNodeCap a \ isCNodeCap b then ->4 else if isThreadCap a \ isThreadCap b then ->5 else if isReplyCap a \ isReplyCap b then ->6 else if isIRQControlCap a \ isIRQControlCap b then ->7 else if isIRQControlCap a \ isIRQHandlerCap b then ->8 else if isIRQHandlerCap a \ isIRQHandlerCap b then (case (a, b) of (IRQHandlerCap a, IRQHandlerCap b) \ ->9 ) else if isArchObjectCap a \ isArchObjectCap b then (case (a, b) of (ArchObjectCap a, ArchObjectCap b) \ ->10 ) else ->11 case \x of ((a@PageCap {}), (b@PageCap {})) -> (a, b) -> ---> let (a, b) = \x in if isPageCap a \ isPageCap b then ->1 else ->2 case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (a, b) -> ---> let (a, b) = \x in if isPageCap a \ isPageCap b then let ptrA = capVPBasePtr a in ->1 else ->2 case \x of NullCap -> c2@(Zombie { capZombiePtr = ptr2 }) -> _ -> ---> let c2 = \x in if isNullCap c2 then ->1 else if isZombie c2 then let ptr2 = capZombiePtr c2 in ->2 else ->3 case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (NullCap, _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> ((IRQHandlerCap { capIRQ = irq }), True, _) -> ((Zombie {}), False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ then let ptr = capEPPtr \v0\; final = \v1\ in ->1 else if isNotificationCap \v0\ then let ptr = capNtfnPtr \v0\; final = \v1\ in ->2 else if isReplyCap \v0\ then ->3 else if isNullCap \v0\ then ->4 else if \v2\ then ->5 else if isCNodeCap \v0\ \ \v1\ then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ in ->6 else if isThreadCap \v0\ \ \v1\ then let tcb = capTCBPtr \v0\ in ->7 else if isZombie \v0\ \ \v1\ then let z = \v0\ in ->8 else if isArchObjectCap \v0\ then let cap = capCap \v0\; final = \v1\ in ->9 else if isIRQHandlerCap \v0\ \ \v1\ then let irq = capIRQ \v0\ in ->10 else if isZombie \v0\ \ \ \v1\ then ->11 else ->12 case \x of (cap@CNodeCap {}) -> (cap@Zombie {}) -> (cap@ThreadCap {}) -> _ -> ---> let cap = \x in if isCNodeCap cap then ->1 else if isZombie cap then ->2 else if isThreadCap cap then ->3 else ->4 case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap {}) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in if isZombie cap then ->1 else if isIRQControlCap cap then ->2 else if isUntypedCap cap then ->3 else if isReplyCap cap then ->4 else if isArchObjectCap cap then let cap = capCap cap in ->5 else ->6 case \x of NullCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in if isNullCap cap then ->1 else if isZombie cap then let ptr = capZombiePtr cap; tp = capZombieType cap; n = capZombieNumber cap in ->2 else if isEndpointCap cap then let ep = capEPPtr cap; b = capEPBadge cap in ->3 else if isArchObjectCap cap then let cap = capCap cap in ->4 else ->5 case \x of cte@(CTE { cteMDBNode = mdb }) -> ---> let cte = \x; mdb = cteMDBNode cte in ->1 case \x of (0, vaddr:attr:_, (pdCap,_):_) -> (0, _, _) -> (1, _, _) -> _ -> ---> let (\v0\, \v1\, \v2\) = \x in if \v0\ = 0 then if length \v1\ > 1 \ length \v2\ > 0 then let vaddr = \v1\ !! 0; attr = \v1\ !! 1; pdCap = fst (\v2\ !! 0) in ->1 else ->2 else if \v0\ = 1 then ->3 else ->4 case \x of (slot, 0) -> (_, bitsLeft) -> ---> let (slot, bitsLeft) = \x in if bitsLeft = 0 then ->1 else ->2 case \x of ((index:bits:args), cap@(CNodeCap {})) -> (_, (CNodeCap {})) -> (_, _) -> ---> let (\v0\, cap) = \x in if isCNodeCap cap then (case \v0\ of (index # bits # args) \ ->1 | _ \ ->2 ) else ->3 case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {}) -> cap@(CNodeCap {}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ -> ---> let cap = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else if isNotificationCap cap \ capNtfnCanSend cap then ->2 else if isReplyCap cap \ \ capReplyMaster cap then ->3 else if isThreadCap cap then ->4 else if isCNodeCap cap then ->5 else if isUntypedCap cap then ->6 else if isIRQControlCap cap then ->7 else if isIRQHandlerCap cap then let irq = capIRQ cap in ->8 else if isArchObjectCap cap then let cap = capCap cap in ->9 else ->10 case \x of (Zombie {}) -> (IRQControlCap) -> cap@(UntypedCap { capBlockSize = b }) -> (ReplyCap {}) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in if isZombie cap then ->1 else if isIRQControlCap cap then ->2 else if isUntypedCap cap then let b = capBlockSize cap in ->3 else if isReplyCap cap then ->4 else if isArchObjectCap cap then let cap = capCap cap in ->5 else ->6 case \x of ((Zombie { capZombieNumber = 0 }), _) -> ((Zombie { capZombiePtr = ptr }), False) -> (z@(Zombie { capZombiePtr = ptr, capZombieNumber = n }), True) -> (_, _) -> ---> let (\v0\, \v1\) = \x in if isZombie \v0\ \ capZombieNumber \v0\ = 0 then ->1 else if isZombie \v0\ \ \ \v1\ then let ptr = capZombiePtr \v0\ in ->2 else if isZombie \v0\ \ \v1\ then let z = \v0\; ptr = capZombiePtr z; n = capZombieNumber z in ->3 else ->4 case \x of ((EndpointCap { capEPPtr = ptr }), final, _) -> ((NotificationCap { capNtfnPtr = ptr }), final, _) -> ((ReplyCap {}), _, _) -> (NullCap, _, _) -> (DomainCap, _, _) -> (_, _, True) -> ((CNodeCap { capCNodePtr = ptr, capCNodeBits = bits }), True, _) -> ((ThreadCap { capTCBPtr = tcb}), True, _) -> (z@(Zombie {}), True, _) -> ((ArchObjectCap { capCap = cap }), final, _) -> (cap@(IRQHandlerCap { capIRQ = irq }), True, _) -> ((Zombie {}), False, _) -> (_, _, _) -> ---> let (\v0\, \v1\, \v2\) = \x in if isEndpointCap \v0\ then let ptr = capEPPtr \v0\; final = \v1\ in ->1 else if isNotificationCap \v0\ then let ptr = capNtfnPtr \v0\; final = \v1\ in ->2 else if isReplyCap \v0\ then ->3 else if isNullCap \v0\ then ->4 else if isDomainCap \v0\ then ->5 else if \v2\ then ->6 else if isCNodeCap \v0\ \ \v1\ then let ptr = capCNodePtr \v0\; bits = capCNodeBits \v0\ in ->7 else if isThreadCap \v0\ \ \v1\ then let tcb = capTCBPtr \v0\ in ->8 else if isZombie \v0\ \ \v1\ then let z = \v0\ in ->9 else if isArchObjectCap \v0\ then let cap = capCap \v0\; final = \v1\ in ->10 else if isIRQHandlerCap \v0\ \ \v1\ then let irq = capIRQ \v0\; cap = \v0\ in ->11 else if isZombie \v0\ \ \ \v1\ then ->12 else ->13 case \x of NullCap -> DomainCap -> (Zombie { capZombiePtr = ptr, capZombieType = tp }) -> (cap@EndpointCap { capEPPtr = ep, capEPBadge = b }) -> (ArchObjectCap cap) -> cap -> ---> let cap = \x in if isNullCap cap then ->1 else if isDomainCap cap then ->2 else if isZombie cap then let ptr = capZombiePtr cap; tp = capZombieType cap; n = capZombieNumber cap in ->3 else if isEndpointCap cap then let ep = capEPPtr cap; b = capEPBadge cap in ->4 else if isArchObjectCap cap then let cap = capCap cap in ->5 else ->6 case \x of NullCap -> DomainCap -> c@(UntypedCap {}) -> c@(EndpointCap {}) -> c@(NotificationCap {}) -> c@(ReplyCap {}) -> c@(CNodeCap {}) -> c@(ThreadCap {}) -> c@IRQControlCap -> c@(IRQHandlerCap {}) -> (ArchObjectCap {capCap = aoCap}) -> c@(Zombie {}) -> ---> let c = \x; aoCap = capCap \x in if isNullCap c then ->1 else if isDomainCap c then ->2 else if isUntypedCap c then ->3 else if isEndpointCap c then ->4 else if isNotificationCap c then ->5 else if isReplyCap c then ->6 else if isCNodeCap c then ->7 else if isThreadCap c then ->8 else if isIRQControlCap c then ->9 else if isIRQHandlerCap c then ->10 else if isArchObjectCap c then ->11 else if isZombie c then ->12 else undefined case \x of cap@(EndpointCap {capEPCanSend=True}) -> cap@(NotificationCap {capNtfnCanSend=True}) -> cap@(ReplyCap {capReplyMaster=False}) -> cap@(ThreadCap {}) -> DomainCap -> cap@(CNodeCap {}) -> cap@(UntypedCap {}) -> IRQControlCap -> (IRQHandlerCap { capIRQ = irq }) -> (ArchObjectCap cap) -> _ -> ---> let cap = \x in if isEndpointCap cap \ capEPCanSend cap then ->1 else if isNotificationCap cap \ capNtfnCanSend cap then ->2 else if isReplyCap cap \ \ capReplyMaster cap then ->3 else if isThreadCap cap then ->4 else if isDomainCap cap then ->5 else if isCNodeCap cap then ->6 else if isUntypedCap cap then ->7 else if isIRQControlCap cap then ->8 else if isIRQHandlerCap cap then let irq = capIRQ cap in ->9 else if isArchObjectCap cap then let cap = capCap cap in ->10 else ->11 case \x of (a@(UntypedCap {}), b) -> ((a@EndpointCap {}), (b@EndpointCap {})) -> ((a@NotificationCap {}), (b@NotificationCap {})) -> ((a@CNodeCap {}), (b@CNodeCap {})) -> ((a@ThreadCap {}), (b@ThreadCap {})) -> ((a@ReplyCap {}), (b@ReplyCap {})) -> (DomainCap, DomainCap) -> (IRQControlCap, IRQControlCap) -> (IRQControlCap, (IRQHandlerCap {})) -> ((IRQHandlerCap a), (IRQHandlerCap b)) -> ((ArchObjectCap a), (ArchObjectCap b)) -> (_, _) -> ---> let (a, b) = \x in if isUntypedCap a then ->1 else if isEndpointCap a \ isEndpointCap b then ->2 else if isNotificationCap a \ isNotificationCap b then ->3 else if isCNodeCap a \ isCNodeCap b then ->4 else if isThreadCap a \ isThreadCap b then ->5 else if isReplyCap a \ isReplyCap b then ->6 else if isDomainCap a \ isDomainCap b then ->7 else if isIRQControlCap a \ isIRQControlCap b then ->8 else if isIRQControlCap a \ isIRQHandlerCap b then ->9 else if isIRQHandlerCap a \ isIRQHandlerCap b then (case (a, b) of (IRQHandlerCap a, IRQHandlerCap b) \ ->10 ) else if isArchObjectCap a \ isArchObjectCap b then (case (a, b) of (ArchObjectCap a, ArchObjectCap b) \ ->11 ) else ->12 case \x of cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> ---> let cap = \x in if isPageDirectoryCap cap then ->1 else if isPageTableCap cap then ->2 else if isPageCap cap then ->3 else if isASIDControlCap cap then ->4 else if isASIDPoolCap cap then ->5 else undefined case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedAddress = Just _ }) -> (PageDirectoryCap { capPDMappedAddress = Nothing }) -> (c@PDPointerTableCap { capPDPTMappedAddress = Just _ }) -> (PDPointerTableCap { capPDPTMappedAddress = Nothing }) -> (c@PML4Cap { capPML4MappedASID = Just _ }) -> (PML4Cap { capPML4MappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@IOPortCap {}) -> IOPortControlCap -> ---> let c = \x in if isPageTableCap c \ capPTMappedAddress c \ None then ->1 else if isPageTableCap c \ capPTMappedAddress c = None then ->2 else if isPageDirectoryCap c \ capPDMappedAddress c \ None then ->3 else if isPageDirectoryCap c \ capPDMappedAddress c = None then ->4 else if isPDPointerTableCap c \ capPDPTMappedAddress c \ None then ->5 else if isPDPointerTableCap c \ capPDPTMappedAddress c = None then ->6 else if isPML4Cap c \ capPML4MappedASID c \ None then ->7 else if isPML4Cap c \ capPML4MappedASID c = None then ->8 else if isPageCap c then ->9 else if isASIDControlCap c then ->10 else if isASIDPoolCap c then ->11 else if isIOPortCap c then ->12 else if isIOPortControlCap c then ->13 else undefined case \x of (c@IOPortCap {}) -> c -> ---> let c = \x in if isIOPortCap c then ->1 else ->2 case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> (cap@PDPointerTableCap { capPDPTBasePtr = ptr }) -> (cap@PML4Cap { capPML4BasePtr = ptr }) -> (cap@IOPortCap {}) -> (cap@IOSpaceCap) -> (cap@IOPageTableCap { capIOPTBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> ---> let cap = \x in if isPageCap cap then ->1 else if isPageTableCap cap then let ptr = capPTBasePtr cap in ->2 else if isPageDirectoryCap cap then let ptr = capPDBasePtr cap in ->3 else if isPDPointerTableCap cap then let ptr = capPDPTBasePtr cap in ->4 else if isPML4Cap cap then let ptr = capPML4BasePtr cap in ->5 else if isIOPortCap cap then ->6 else if isIOSpaceCap cap then ->7 else if isIOPageTableCap cap then let ptr = capIOPTBasePtr cap in ->8 else if isASIDControlCap cap then ->9 else if isASIDPoolCap cap then let base = capASIDBase cap; ptr = capASIDPool cap in ->10 else undefined case \x of (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerIOAPIC, index:depth:ioapic:pin:level:polarity:irqW:_, cnode:_) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerIOAPIC, _, _) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerMSI, index:depth:pciBus:pciDev:pciFunc:handle:irqW:_, cnode:_) -> (ArchInvocationLabel ArchLabels.X64IRQIssueIRQHandlerMSI, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, index#depth#ioapic#pin#level#polarity#irqW#_, cnode#_) => ->1 | (ArchInvocationLabel X64IRQIssueIRQHandlerIOAPIC, _, _) => ->2 | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, index#depth#pciBus#pciDev#pciFunc#handle#irqW#_, cnode#_) => ->3 | (ArchInvocationLabel X64IRQIssueIRQHandlerMSI, _, _) => ->4 | _ => ->5 case \x of (ArchInv.IssueIRQHandlerIOAPIC (IRQ irq) destSlot srcSlot ioapic pin level polarity vector) -> (ArchInv.IssueIRQHandlerMSI (IRQ irq) destSlot srcSlot pciBus pciDev pciFunc handle) -> ---> let inv = \x in case inv of (IssueIRQHandlerIOAPIC irq destSlot srcSlot ioapic pin level polarity vector) => ->1 | (IssueIRQHandlerMSI irq destSlot srcSlot pciBus pciDev pciFunc handle) => ->2 case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> (cap@PDPointerTableCap { capPDPTBasePtr = ptr }) -> (cap@PML4Cap { capPML4BasePtr = ptr }) -> (cap@IOPortCap {}) -> (cap@IOSpaceCap {}) -> (cap@IOPageTableCap { capIOPTBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> ---> let cap = \x in if isPageCap cap then ->1 else if isPageTableCap cap then let ptr = capPTBasePtr cap in ->2 else if isPageDirectoryCap cap then let ptr = capPDBasePtr cap in ->3 else if isPDPointerTableCap cap then let ptr = capPDPTBasePtr cap in ->4 else if isPML4Cap cap then let ptr = capPML4BasePtr cap in ->5 else if isIOPortCap cap then ->6 else if isIOSpaceCap cap then ->7 else if isIOPageTableCap cap then let ptr = capIOPTBasePtr cap in ->8 else if isASIDControlCap cap then ->9 else if isASIDPoolCap cap then let base = capASIDBase cap; ptr = capASIDPool cap in ->10 else undefined case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.HugePageObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> Arch.Types.PDPointerTableObject -> Arch.Types.PML4Object -> ---> let t = \x in case t of APIObjectType _ => ->1 | SmallPageObject => ->2 | LargePageObject => ->3 | HugePageObject => ->4 | PageTableObject => ->5 | PageDirectoryObject => ->6 | PDPointerTableObject => ->7 | PML4Object => ->8 case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> ((a@PDPointerTableCap {}), (b@PDPointerTableCap {})) -> ((a@PML4Cap {}), (b@PML4Cap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@IOPortCap {}), (b@IOPortCap {})) -> (IOPortControlCap, IOPortControlCap) -> (IOPortControlCap, (IOPortCap {})) -> (_, _) -> ---> let (a,b) = \x in if isPageCap a \ isPageCap b then ->1 else if isPageTableCap a \ isPageTableCap b then ->2 else if isPageDirectoryCap a \ isPageDirectoryCap b then ->3 else if isPDPointerTableCap a \ isPDPointerTableCap b then ->4 else if isPML4Cap a \ isPML4Cap b then ->5 else if isASIDControlCap a \ isASIDControlCap b then ->6 else if isASIDPoolCap a \ isASIDPoolCap b then ->7 else if isIOPortCap a \ isIOPortCap b then ->8 else if isIOPortControlCap a \ isIOPortControlCap b then ->9 else if isIOPortControlCap a \ isIOPortCap b then ->10 else ->11 case \x of (oper@(InvokeIOPort _)) -> (oper@(InvokeIOPortControl _)) -> oper -> ---> let oper = \x in case oper of InvokeIOPort _ => ->1 | InvokeIOPortControl _ => ->2 | _ => ->3 case \x of (cap@PageCap {}) -> _ -> ---> let cap = \x in if isPageCap cap then ->1 else ->2 case \x of (ArchInvocationLabel X64IOPortControlIssue, f:l:index:depth:_, cnode:_) -> (ArchInvocationLabel X64IOPortControlIssue, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64IOPortControlIssue, f#l#index#depth#_, cnode#_) => ->1 | (ArchInvocationLabel X64IOPortControlIssue, _, _) => ->2 | _ => ->3 case \x of (ArchInvocationLabel X64PDPTMap, vaddr':attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PDPTMap, _, _) -> (ArchInvocationLabel X64PDPTUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64PDPTMap, vaddr'#attr#_, (vspaceCap,_)#_) => ->1 | (ArchInvocationLabel X64PDPTMap, _, _) => ->2 | (ArchInvocationLabel X64PDPTUnmap, _, _) => ->3 | _ => ->4 case \x of (ArchInvocationLabel X64PageDirectoryMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64PageDirectoryMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1 | (ArchInvocationLabel X64PageDirectoryMap, _, _) => ->2 | (ArchInvocationLabel X64PageDirectoryUnmap, _, _) => ->3 | _ => ->4 case \x of (ArchInvocationLabel X64PageTableMap, vaddr':attr:_, (pml4Cap,_):_) -> (ArchInvocationLabel X64PageTableMap, _, _) -> (ArchInvocationLabel X64PageTableUnmap, _, _) -> _ -> --->let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64PageTableMap, vaddr'#attr#_, (pml4Cap,_)#_) => ->1 | (ArchInvocationLabel X64PageTableMap, _, _) => ->2 | (ArchInvocationLabel X64PageTableUnmap, _, _) => ->3 | _ => ->4 case \x of (ArchInvocationLabel X64ASIDControlMakePool, index:depth:_, (untyped,parentSlot):(croot,_):_) -> (ArchInvocationLabel X64ASIDControlMakePool, _, _) -> _ -> ---> let (label, args, extraCaps) = \x in case (label, args, extraCaps) of (ArchInvocationLabel X64ASIDControlMakePool, index#depth#_, (untyped,parentSlot)#(croot,_):_) => ->1 | (ArchInvocationLabel X64ASIDControlMakePool, _, _) => ->2 | _ => ->3 case \x of (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot):_) -> (ArchInvocationLabel X64ASIDPoolAssign, _) -> _ -> ---> let (label, extraCaps) = \x in case (label, extraCaps) of (ArchInvocationLabel X64ASIDPoolAssign, (vspaceCap,vspaceCapSlot)#_) => ->1 | (ArchInvocationLabel X64ASIDPoolAssign, _) => ->2 | _ => ->3 case \x of cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(PageCap {}) -> ASIDControlCap -> cap@(ASIDPoolCap {}) -> _ -> ---> let cap = \x in if isPDPointerTableCap cap then ->1 else if isPageDirectoryCap cap then ->2 else if isPageTableCap cap then ->3 else if isPageCap cap then ->4 else if isASIDPoolCap cap then ->5 else ->6 case \x of (cap@(IOPortCap { capIOPortFirstPort = first_allowed, capIOPortLastPort = last_allowed })) -> _ -> ---> let cap = \x in if isIOPortCap cap then let first_allowed = capIOPortFirstPort cap; last_allowed = capIOPortLastPort cap in ->1 else ->2 case \x of (ArchInvocationLabel X64IOPortIn8, port':_) -> (ArchInvocationLabel X64IOPortIn8, _) -> (ArchInvocationLabel X64IOPortIn16, port':_) -> (ArchInvocationLabel X64IOPortIn16, _) -> (ArchInvocationLabel X64IOPortIn32, port':_) -> (ArchInvocationLabel X64IOPortIn32, _) -> (ArchInvocationLabel X64IOPortOut8, port':out:_) -> (ArchInvocationLabel X64IOPortOut8, _) -> (ArchInvocationLabel X64IOPortOut16, port':out:_) -> (ArchInvocationLabel X64IOPortOut16, _) -> (ArchInvocationLabel X64IOPortOut32, port':out:_) -> (ArchInvocationLabel X64IOPortOut32, _) -> (_, _) -> ---> let (label, args) = \x in case (label, args) of (ArchInvocationLabel X64IOPortIn8, port'#_) => ->1 | (ArchInvocationLabel X64IOPortIn8, _) => ->2 | (ArchInvocationLabel X64IOPortIn16, port'#_) => ->3 | (ArchInvocationLabel X64IOPortIn16, _) => ->4 | (ArchInvocationLabel X64IOPortIn32, port'#_) => ->5 | (ArchInvocationLabel X64IOPortIn32, _) => ->6 | (ArchInvocationLabel X64IOPortOut8, port'#out:_) => ->7 | (ArchInvocationLabel X64IOPortOut8, _) => ->8 | (ArchInvocationLabel X64IOPortOut16, port'#out#_) => ->9 | (ArchInvocationLabel X64IOPortOut16, _) => ->10 | (ArchInvocationLabel X64IOPortOut32, port'#out#_) => ->11 | (ArchInvocationLabel X64IOPortOut32, _) => ->12 | _ => ->13 case \x of cap@(IOPortCap {}) -> _ -> ---> let cap = \x in if isIOPortCap cap then ->1 else ->2 case \x of cap@(IOPortCap {}) -> IOPortControlCap -> _ -> ---> let cap = \x in if isIOPortCap cap then ->1 else if isIOPortControlCap cap then ->2 else ->3 case \x of (cap @ (CNodeCap {})) -> (cap @ (ThreadCap {})) -> (cap @ (Zombie {})) -> _ -> ---> let cap = \x in if isCNodeCap cap then ->1 else if isThreadCap cap then ->2 else if isZombie cap then ->3 else ->4 case \x of ArchInv.IOPortIn8 -> ArchInv.IOPortIn16 -> ArchInv.IOPortIn32 -> ArchInv.IOPortOut8 w -> ArchInv.IOPortOut16 w -> ArchInv.IOPortOut32 w -> ---> let port_data = \x in case port_data of IOPortIn8 => ->1 | IOPortIn16 => ->2 | IOPortIn32 => ->3 | IOPortOut8 w => ->4 | IOPortOut16 w => ->5 | IOPortOut32 w => ->6 case \x of (ArchInvocationLabel X64PageMap, vaddr:rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageMap, _, _) -> (ArchInvocationLabel X64PageRemap, rightsMask:attr:_, (vspaceCap,_):_) -> (ArchInvocationLabel X64PageRemap, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> (ArchInvocationLabel X64PageGetAddress, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in case (ilabel, args, extraCaps) of (ArchInvocationLabel X64PageMap, vaddr#rightsMask#attr#_, (vspaceCap, _)#_) => ->1 | (ArchInvocationLabel X64PageMap, _, _) => ->2 | (ArchInvocationLabel X64PageRemap, rightsMask#attr#_, (vspaceCap, _)#_) => ->3 | (ArchInvocationLabel X64PageRemap, _, _) => ->4 | (ArchInvocationLabel X64PageUnmap, _, _) => ->5 | (ArchInvocationLabel X64PageGetAddress, _, _) => ->6 | _ => ->7 case \x of (ArchInvocationLabel X64IOPageTableMap, ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64IOPageTableMap, _, _) -> (ArchInvocationLabel X64IOPageTableUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in case (ilabel, args, extraCaps) of (ArchInvocationLabel X64IOPageTableMap, ioaddr#_, (iospaceCap,_)#_) => ->1 | (ArchInvocationLabel X64IOPageTableMap, _, _) => ->2 | (ArchInvocationLabel X64IOPageTableUnmap, _, _) => ->3 | _ => ->4 case \x of (ArchInvocationLabel X64PageMapIO, rw:ioaddr:_, (iospaceCap,_):_) -> (ArchInvocationLabel X64PageMapIO, _, _) -> (ArchInvocationLabel X64PageUnmap, _, _) -> _ -> ---> let (ilabel, args, extraCaps) = \x in case (ilabel, args, extraCaps) of (ArchInvocationLabel X64PageMapIO, rw:ioaddr#_, (iospaceCap,_)#_) => ->1 | (ArchInvocationLabel X64PageMapIO, _, _) => ->2 | (ArchInvocationLabel X64PageUnmap, _, _) => ->3 | _ => ->4 case \x of cap@(PDPointerTableCap {}) -> _ -> ---> let cap = \x in if isPDPointerTableCap cap then ->1 else ->2 case \x of cap@(PageDirectoryCap {}) -> _ -> ---> let cap = \x in if isPageDirectoryCap cap then ->1 else ->2 case \x of cap@(PageTableCap {}) -> _ -> ---> let cap = \x in if isPageTableCap cap then ->1 else ->2 case \x of cap@(ASIDPoolCap {}) -> _ -> ---> let cap = \x in if isASIDPoolCap cap then ->1 else ->2 case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> cap@(IOPageTableCap {}) -> cap@(PML4Cap {}) -> _ -> ---> let cap = \x in if isPageCap cap then ->1 else if isPDPointerTableCap cap then ->2 else if isPageDirectoryCap cap then ->3 else if isPageTableCap cap then ->4 else if isASIDControlCap cap then ->5 else if isASIDPoolCap cap then ->6 else if isIOPageTableCap cap then ->7 else if isPML4Cap cap then ->8 else ->9 case \x of cap@(PageCap {}) -> cap@(PDPointerTableCap {}) -> cap@(PageDirectoryCap {}) -> cap@(PageTableCap {}) -> cap@(ASIDControlCap {}) -> cap@(ASIDPoolCap {}) -> (PML4Cap {}) -> _ -> ---> let cap = \x in if isPageCap cap then ->1 else if isPDPointerTableCap cap then ->2 else if isPageDirectoryCap cap then ->3 else if isPageTableCap cap then ->4 else if isASIDControlCap cap then ->5 else if isASIDPoolCap cap then ->6 else if isPML4Cap cap then ->7 else ->8 case \x of cap@(IOPageTableCap {}) -> _ -> ---> let cap = \x in if isIOPageTableCap then ->1 else ->2 case \x of (cap@UntypedCap {}) -> _ -> ---> let cap = \x in if isUntypedCap cap then ->1 else ->2 case \x of cap@(PageCap {}) -> _ -> ---> let cap = \x in if isPageCap cap then ->1 else ->2 case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) -> ---> let \v0\ = \x in case \v0\ of PageMap asid cap ct ctSlot entries => ->1 | PageRemap entries => ->2 | PageUnmap cap ctSlot => ->3 | PageIOMap cap cptr ctdpte slot => ->4 | PageIOUnmap (ArchObjectCap cap) ctSlot => if isPageCap cap then ->5 else ->6 | PageIOUnmap _ _ => ->6 | PageGetAddr ptr => ->7 case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in if isUntypedCap \v0\ \ capBlockSize \v0\ == objBits pool then ->1 else ->2 case \x of (cap@IOPageTableCap {}) -> _ -> ---> let cap = \x in if isIOPageTableCap cap then ->1 else ->2 case \x of cap@(PageCap {}) -> _ -> ---> let cap = \x in if isPageCap cap then ->1 else ->2 case \x of (PageMap asid cap ctSlot entries) -> (PageRemap entries) -> (PageUnmap cap ctSlot) -> (PageIOMap cap cptr vtdpte slot) -> (PageIOUnmap (ArchObjectCap cap@PageCap {}) ctSlot) -> (PageIOUnmap _ _) -> (PageGetAddr ptr) -> ---> let \v0\ = \x in case \v0\ of PageMap asid cap ct ctSlot entries => ->1 | PageRemap entries => ->2 | PageUnmap cap ctSlot => ->3 | PageIOMap cap cptr ctdpte slot => ->4 | PageIOUnmap (ArchObjectCap cap) ctSlot => if isPageCap cap then ->5 else ->6 | PageIOUnmap _ _ => ->6 | PageGetAddr ptr => ->7 case \x of UntypedCap {} | capBlockSize untyped == objBits pool -> _ -> ---> let \v0\ = \x in if isUntypedCap \v0\ \ capBlockSize \v0\ == objBits pool then ->1 else ->2 case \x of (cap@IOPageTableCap {}) -> _ -> ---> let cap = \x in if isIOPageTableCap cap then ->1 else ->2 case \x of (X64NoHypFaults) -> ---> let hyp = \x in case hyp of X64NoHypFaults => ->1 case \x of ((a@PageCap { capVPBasePtr = ptrA }), (b@PageCap {})) -> (IOPortControlCap, (IOPortCap {})) -> (a, b) -> ---> let (a, b) = \x in if isPageCap a \ isPageCap b then let ptrA = capVPBasePtr a in ->1 else if isIOPortControlCap a \ isIOPortCap b then -> 2 else ->3 case \x of cap@(VCPUCap {}) -> _ -> ---> let cap = \x in if isVCPUCap cap then -> 1 else ->2 case \x of ((field:_), cap@(VCPUCap {})) -> (_, _) -> ---> let (ls, cap) = \x in if isVCPUCap cap \ length ls > 0 then let field = ls !! 0 in ->1 else ->2 case \x of ((field:val:_), cap@(VCPUCap {})) -> (_, _) -> ---> let (ls, cap) = \x in if isVCPUCap cap \ length ls > 1 then let field = ls !! 0; val = ls !! 1 in ->1 else ->2 case \x of (c@PageTableCap { capPTMappedAddress = Just _ }) -> (PageTableCap { capPTMappedAddress = Nothing }) -> (c@PageDirectoryCap { capPDMappedASID = Just _ }) -> (PageDirectoryCap { capPDMappedASID = Nothing }) -> (c@PageCap {}) -> c@ASIDControlCap -> (c@ASIDPoolCap {}) -> (c@VCPUCap {}) -> ---> let c = \x in if isPageTableCap c \ capPTMappedAddress c \ None then ->1 else if isPageTableCap c \ capPTMappedAddress c = None then ->2 else if isPageDirectoryCap c \ capPDMappedASID c \ None then ->3 else if isPageDirectoryCap c \ capPDMappedASID c = None then ->4 else if isPageCap c then ->5 else if isASIDControlCap c then ->6 else if isASIDPoolCap c then ->7 else if isVCPUCap c then ->8 else undefined case \x of ((ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }), True) -> ((PageDirectoryCap { capPDMappedASID = Just a, capPDBasePtr = ptr }), True) -> ((PageTableCap { capPTMappedAddress = Just (a, v), capPTBasePtr = ptr }), True) -> ((cap@PageCap { capVPMappedAddress = Just (a, v), capVPSize = s, capVPBasePtr = ptr }), _) -> ((VCPUCap {}), _) -> (_, _) -> ---> let (cap, bl) = \x in if isASIDPoolCap cap \ bl then let b = capASIDBase cap; ptr = capASIDPool cap in ->1 else if isPageDirectoryCap cap \ bl \ capPDMappedASID cap \ None then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap in ->2 else if isPageTableCap cap \ bl \ capPTMappedAddress cap \ None then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap in ->3 else if isPageCap cap \ capVPMappedAddress cap \ None then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap in ->4 else if isVCPUCap cap then ->5 else ->6 case \x of (cap@PageCap {}) -> (cap@PageTableCap { capPTBasePtr = ptr }) -> (cap@PageDirectoryCap { capPDBasePtr = ptr }) -> ASIDControlCap -> (cap@ASIDPoolCap { capASIDBase = base, capASIDPool = ptr }) -> (VCPUCap {}) -> ---> let cap = \x in if isPageCap cap then ->1 else if isPageTableCap cap then let ptr = capPTBasePtr cap in ->2 else if isPageDirectoryCap cap then let ptr = capPDBasePtr cap in ->3 else if isASIDControlCap cap then ->4 else if isASIDPoolCap cap then let base = capASIDBase cap; ptr = capASIDPool cap in ->5 else if isVCPUCap cap then ->6 else undefined case \x of ((a@PageCap {}), (b@PageCap {})) -> ((a@PageTableCap {}), (b@PageTableCap {})) -> ((a@PageDirectoryCap {}), (b@PageDirectoryCap {})) -> (ASIDControlCap, ASIDControlCap) -> ((a@ASIDPoolCap {}), (b@ASIDPoolCap {})) -> ((a@VCPUCap {}), (b@VCPUCap {})) -> (_, _) -> ---> let (a, b) = \x in if isPageCap a \ isPageCap b then ->1 else if isPageTableCap a \ isPageTableCap b then ->2 else if isPageDirectoryCap a \ isPageDirectoryCap b then ->3 else if isASIDControlCap a \ isASIDControlCap b then ->4 else if isASIDPoolCap a \ isASIDPoolCap b then ->5 else if isVCPUCap a \ isVCPUCap b then ->6 else ->7 case \x of Arch.Types.APIObjectType _ -> Arch.Types.SmallPageObject -> Arch.Types.LargePageObject -> Arch.Types.SectionObject -> Arch.Types.SuperSectionObject -> Arch.Types.PageTableObject -> Arch.Types.PageDirectoryObject -> Arch.Types.VCPUObject -> ---> case \x of Arch.Types.APIObjectType \v0\ \ ->1 | Arch.Types.SmallPageObject \ ->2 | Arch.Types.LargePageObject \ ->3 | Arch.Types.SectionObject \ ->4 | Arch.Types.SuperSectionObject \ ->5 | Arch.Types.PageTableObject \ ->6 | Arch.Types.PageDirectoryObject \ ->7 | Arch.Type.VCPUObject \ -> 8 case \x of ArchInv.InvokeVCPU iv -> _ -> ---> let inv = \x in case inv of ArchInv.InvokeVCPU iv \