API tools faq
paste
Guest User

Untitled

a guest
Jun 23rd, 2018
85
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 41.84 KB | None | 0 0
raw download clone embed print report
  1. Sub-expression "(fun
  2. lemma : M.memEffect m (step_sem_tiered ge e s MCFG r) =
  3. idM
  4. (M.memEffect m (step_sem_tiered ge e s MCFG r))
  5. =>
  6. reflexive_proper Classes.equiv
  7. (M.memEffect m (step_sem_tiered ge e s MCFG r))
  8. (idM (M.memEffect m (step_sem_tiered ge e s MCFG r)))
  9. lemma
  10. (M.memEffect m
  11. (step_sem_tiered ge e s (monomap cfgp MCFG) r))
  12. (M.memEffect m
  13. (step_sem_tiered ge e s (monomap cfgp MCFG) r))
  14. (eq_proper_proxy
  15. (M.memEffect m
  16. (step_sem_tiered ge e s (monomap cfgp MCFG) r))))
  17. matchM
  18. (eq_ind_r
  19. (Classes.equiv
  20. (idM (M.memEffect m (step_sem_tiered ge e s MCFG r))))
  21. match
  22. r as i
  23. return
  24. (match
  25. match
  26. match i with
  27. | IRDone v => Ret (Event:=IO.IO) v
  28. | IREnterFunction _ _ =>
  29. bindM (execInterpreter ge e s MCFG i)
  30. (fun rnext : InterpreterResult =>
  31. step_sem_tiered ge e s MCFG rnext)
  32. | IRReturnFunction _ =>
  33. bindM (execInterpreter ge e s MCFG i)
  34. (fun rnext : InterpreterResult =>
  35. step_sem_tiered ge e s MCFG rnext)
  36. | IRResumeFunction _ =>
  37. bindM (execInterpreter ge e s MCFG i)
  38. (fun rnext : InterpreterResult =>
  39. step_sem_tiered ge e s MCFG rnext)
  40. end
  41. with
  42. | Ret x => Ret (Event:=IO.IO) (m, x)
  43. | @Vis _ _ Y io k =>
  44. match M.mem_step io m with
  45. | inl _ =>
  46. Err (Event:=IO.IO) (X:=
  47. M.memory * dvalue)
  48. "uninterpretiable IO call "
  49. | inr (m', v) =>
  50. Trace.Tau (M.memEffect m' (k v))
  51. end
  52. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  53. | Err e =>
  54. Err (Event:=IO.IO) (X:=M.memory * dvalue) e
  55. end
  56. with
  57. | Ret x => Ret x
  58. | @Vis _ _ Y e k => Vis e k
  59. | Trace.Tau k => Trace.Tau k
  60. | Err s => Err s
  61. end
  62. ≡ match
  63. match
  64. match i with
  65. | IRDone v => Ret (Event:=IO.IO) v
  66. | IREnterFunction _ _ =>
  67. bindM
  68. (execInterpreter ge e s
  69. (monomap cfgp MCFG) i)
  70. (fun rnext : InterpreterResult =>
  71. step_sem_tiered ge e s
  72. (monomap cfgp MCFG) rnext)
  73. | IRReturnFunction _ =>
  74. bindM
  75. (execInterpreter ge e s
  76. (monomap cfgp MCFG) i)
  77. (fun rnext : InterpreterResult =>
  78. step_sem_tiered ge e s
  79. (monomap cfgp MCFG) rnext)
  80. | IRResumeFunction _ =>
  81. bindM
  82. (execInterpreter ge e s
  83. (monomap cfgp MCFG) i)
  84. (fun rnext : InterpreterResult =>
  85. step_sem_tiered ge e s
  86. (monomap cfgp MCFG) rnext)
  87. end
  88. with
  89. | Ret x => Ret (Event:=IO.IO) (m, x)
  90. | @Vis _ _ Y io k =>
  91. match M.mem_step io m with
  92. | inl _ =>
  93. Err (Event:=IO.IO)
  94. (X:=M.memory * dvalue)
  95. "uninterpretiable IO call "
  96. | inr (m', v) =>
  97. Trace.Tau (M.memEffect m' (k v))
  98. end
  99. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  100. | Err e =>
  101. Err (Event:=IO.IO) (X:=M.memory * dvalue) e
  102. end
  103. with
  104. | Ret x => Ret x
  105. | @Vis _ _ Y e k => Vis e k
  106. | Trace.Tau k => Trace.Tau k
  107. | Err s => Err s
  108. end)
  109. with
  110. | IRDone v => EquivRet
  111. | IREnterFunction fnid args =>
  112. ?X1361@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH;
  113. __:=ge; __:=e; __:=s; __:=MCFG; __:=fnid;
  114. __:=args; __:=m}
  115. | IRReturnFunction fres =>
  116. match
  117. fres as f
  118. return
  119. (match
  120. match
  121. match
  122. execInterpreter ge e s MCFG
  123. (IRReturnFunction f)
  124. with
  125. | Ret x =>
  126. Trace.Tau
  127. (step_sem_tiered ge e s MCFG x)
  128. | @Vis _ _ Y e0 k =>
  129. Vis e0
  130. (fun y : Y =>
  131. (cofix
  132. go (s : M IO.IO InterpreterResult) :
  133. M IO.IO dvalue :=
  134. match s with
  135. | Ret x =>
  136. Trace.Tau
  137. (step_sem_tiered ge e s
  138. MCFG x)
  139. | @Vis _ _ Y0 e k0 =>
  140. Vis e
  141. (fun y0 : Y0 => go (k0 y0))
  142. | Trace.Tau k0 =>
  143. Trace.Tau (go k0)
  144. | Err s0 =>
  145. Err (Event:=IO.IO)
  146. (X:=dvalue) s0
  147. end) (k y))
  148. | Trace.Tau k =>
  149. Trace.Tau
  150. ((cofix
  151. go (s : M IO.IO InterpreterResult) :
  152. M IO.IO dvalue :=
  153. match s with
  154. | Ret x =>
  155. Trace.Tau
  156. (step_sem_tiered ge e s
  157. MCFG x)
  158. | @Vis _ _ Y e k0 =>
  159. Vis e
  160. (fun y : Y => go (k0 y))
  161. | Trace.Tau k0 =>
  162. Trace.Tau (go k0)
  163. | Err s0 =>
  164. Err (Event:=IO.IO)
  165. (X:=dvalue) s0
  166. end) k)
  167. | Err s => Err (Event:=IO.IO) (X:=dvalue) s
  168. end
  169. with
  170. | Ret x => Ret (Event:=IO.IO) (m, x)
  171. | @Vis _ _ Y io k =>
  172. match M.mem_step io m with
  173. | inl _ =>
  174. Err (Event:=IO.IO)
  175. (X:=M.memory * dvalue)
  176. "uninterpretiable IO call "
  177. | inr (m', v) =>
  178. Trace.Tau (M.memEffect m' (k v))
  179. end
  180. | Trace.Tau x' =>
  181. Trace.Tau (M.memEffect m x')
  182. | Err e =>
  183. Err (Event:=IO.IO) (X:=
  184. M.memory * dvalue) e
  185. end
  186. with
  187. | Ret x => Ret x
  188. | @Vis _ _ Y e k => Vis e k
  189. | Trace.Tau k => Trace.Tau k
  190. | Err s => Err s
  191. end
  192. ≡ match
  193. match
  194. match
  195. execInterpreter ge e s
  196. (monomap cfgp MCFG)
  197. (IRReturnFunction f)
  198. with
  199. | Ret x =>
  200. Trace.Tau
  201. (step_sem_tiered ge e s
  202. (monomap cfgp MCFG) x)
  203. | @Vis _ _ Y e0 k =>
  204. Vis e0
  205. (fun y : Y =>
  206. (cofix
  207. go (s :
  208. M IO.IO InterpreterResult) :
  209. M IO.IO dvalue :=
  210. match s with
  211. | Ret x =>
  212. Trace.Tau
  213. (step_sem_tiered ge e s
  214. (monomap cfgp MCFG) x)
  215. | @Vis _ _ Y0 e k0 =>
  216. Vis e
  217. (fun y0 : Y0 => go (k0 y0))
  218. | Trace.Tau k0 =>
  219. Trace.Tau (go k0)
  220. | Err s0 =>
  221. Err (Event:=IO.IO)
  222. (X:=dvalue) s0
  223. end)
  224. (k y))
  225. | Trace.Tau k =>
  226. Trace.Tau
  227. ((cofix
  228. go (s :
  229. M IO.IO InterpreterResult) :
  230. M IO.IO dvalue :=
  231. match s with
  232. | Ret x =>
  233. Trace.Tau
  234. (step_sem_tiered ge e s
  235. (monomap cfgp MCFG) x)
  236. | @Vis _ _ Y e k0 =>
  237. Vis e
  238. (fun y : Y => go (k0 y))
  239. | Trace.Tau k0 =>
  240. Trace.Tau (go k0)
  241. | Err s0 =>
  242. Err (Event:=IO.IO)
  243. (X:=dvalue) s0
  244. end) k)
  245. | Err s =>
  246. Err (Event:=IO.IO) (X:=dvalue) s
  247. end
  248. with
  249. | Ret x => Ret (Event:=IO.IO) (m, x)
  250. | @Vis _ _ Y io k =>
  251. match M.mem_step io m with
  252. | inl _ =>
  253. Err (Event:=IO.IO)
  254. (X:=M.memory * dvalue)
  255. "uninterpretiable IO call "
  256. | inr (m', v) =>
  257. Trace.Tau (M.memEffect m' (k v))
  258. end
  259. | Trace.Tau x' =>
  260. Trace.Tau (M.memEffect m x')
  261. | Err e =>
  262. Err (Event:=IO.IO)
  263. (X:=M.memory * dvalue) e
  264. end
  265. with
  266. | Ret x => Ret x
  267. | @Vis _ _ Y e k => Vis e k
  268. | Trace.Tau k => Trace.Tau k
  269. | Err s => Err s
  270. end)
  271. with
  272. | FRReturn d =>
  273. match
  274. s as l
  275. return
  276. (match
  277. match
  278. match
  279. execInterpreter ge e l MCFG
  280. (IRReturnFunction (FRReturn d))
  281. with
  282. | Ret x =>
  283. Trace.Tau
  284. (step_sem_tiered ge e l MCFG x)
  285. | @Vis _ _ Y e0 k =>
  286. Vis e0
  287. (fun y : Y =>
  288. (cofix
  289. go (s :
  290. M IO.IO InterpreterResult) :
  291. M IO.IO dvalue :=
  292. match s with
  293. | Ret x =>
  294. Trace.Tau
  295. (step_sem_tiered ge e l
  296. MCFG x)
  297. | @Vis _ _ Y0 e k0 =>
  298. Vis e
  299. (fun y0 : Y0 => go (k0 y0))
  300. | Trace.Tau k0 =>
  301. Trace.Tau (go k0)
  302. | Err s0 =>
  303. Err (Event:=IO.IO)
  304. (X:=dvalue) s0
  305. end)
  306. (k y))
  307. | Trace.Tau k =>
  308. Trace.Tau
  309. ((cofix
  310. go (s :
  311. M IO.IO InterpreterResult) :
  312. M IO.IO dvalue :=
  313. match s with
  314. | Ret x =>
  315. Trace.Tau
  316. (step_sem_tiered ge e l
  317. MCFG x)
  318. | @Vis _ _ Y e k0 =>
  319. Vis e
  320. (fun y : Y => go (k0 y))
  321. | Trace.Tau k0 =>
  322. Trace.Tau (go k0)
  323. | Err s0 =>
  324. Err (Event:=IO.IO)
  325. (X:=dvalue) s0
  326. end) k)
  327. | Err s =>
  328. Err (Event:=IO.IO) (X:=dvalue) s
  329. end
  330. with
  331. | Ret x => Ret (Event:=IO.IO) (m, x)
  332. | @Vis _ _ Y io k =>
  333. match M.mem_step io m with
  334. | inl _ =>
  335. Err (Event:=IO.IO)
  336. (X:=M.memory * dvalue)
  337. "uninterpretiable IO call "
  338. | inr (m', v) =>
  339. Trace.Tau (M.memEffect m' (k v))
  340. end
  341. | Trace.Tau x' =>
  342. Trace.Tau (M.memEffect m x')
  343. | Err e =>
  344. Err (Event:=IO.IO)
  345. (X:=M.memory * dvalue) e
  346. end
  347. with
  348. | Ret x => Ret x
  349. | @Vis _ _ Y e k => Vis e k
  350. | Trace.Tau k => Trace.Tau k
  351. | Err s => Err s
  352. end
  353. ≡ match
  354. match
  355. match
  356. execInterpreter ge e l
  357. (monomap cfgp MCFG)
  358. (IRReturnFunction (FRReturn d))
  359. with
  360. | Ret x =>
  361. Trace.Tau
  362. (step_sem_tiered ge e l
  363. (monomap cfgp MCFG) x)
  364. | @Vis _ _ Y e0 k =>
  365. Vis e0
  366. (fun y : Y =>
  367. (cofix
  368. go
  369. (s :
  370. M IO.IO InterpreterResult) :
  371. M IO.IO dvalue :=
  372. match s with
  373. | Ret x =>
  374. Trace.Tau
  375. (step_sem_tiered ge e l
  376. (monomap cfgp MCFG) x)
  377. | @Vis _ _ Y0 e k0 =>
  378. Vis e
  379. (fun y0 : Y0 => go (k0 y0))
  380. | Trace.Tau k0 =>
  381. Trace.Tau (go k0)
  382. | Err s0 =>
  383. Err (Event:=IO.IO)
  384. (X:=dvalue) s0
  385. end)
  386. (k y))
  387. | Trace.Tau k =>
  388. Trace.Tau
  389. ((cofix
  390. go
  391. (s :
  392. M IO.IO InterpreterResult) :
  393. M IO.IO dvalue :=
  394. match s with
  395. | Ret x =>
  396. Trace.Tau
  397. (step_sem_tiered ge e l
  398. (monomap cfgp MCFG) x)
  399. | @Vis _ _ Y e k0 =>
  400. Vis e
  401. (fun y : Y => go (k0 y))
  402. | Trace.Tau k0 =>
  403. Trace.Tau (go k0)
  404. | Err s0 =>
  405. Err (Event:=IO.IO)
  406. (X:=dvalue) s0
  407. end) k)
  408. | Err s =>
  409. Err (Event:=IO.IO) (X:=dvalue) s
  410. end
  411. with
  412. | Ret x => Ret (Event:=IO.IO) (m, x)
  413. | @Vis _ _ Y io k =>
  414. match M.mem_step io m with
  415. | inl _ =>
  416. Err (Event:=IO.IO)
  417. (X:=
  418. M.memory * dvalue)
  419. "uninterpretiable IO call "
  420. | inr (m', v) =>
  421. Trace.Tau
  422. (M.memEffect m' (k v))
  423. end
  424. | Trace.Tau x' =>
  425. Trace.Tau (M.memEffect m x')
  426. | Err e =>
  427. Err (Event:=IO.IO)
  428. (X:=M.memory * dvalue) e
  429. end
  430. with
  431. | Ret x => Ret x
  432. | @Vis _ _ Y e k => Vis e k
  433. | Trace.Tau k => Trace.Tau k
  434. | Err s => Err s
  435. end)
  436. with
  437. | [] => EquivTau (CIH ge e [] MCFG (IRDone d) m)
  438. | f :: s0 =>
  439. ?X1402@{__:=cfgp; __:=PRESERVE_CFG_EFFECT;
  440. __:=CIH; __:=ge; __:=e; __:=f;
  441. __:=s0; __:=MCFG; __:=d; __:=m}
  442. end
  443. | FRReturnVoid =>
  444. ?X1391@{__:=cfgp; __:=PRESERVE_CFG_EFFECT;
  445. __:=CIH; __:=ge; __:=e; __:=s; __:=MCFG;
  446. __:=m}
  447. | FRCall f l i p =>
  448. ?X1392@{__:=cfgp; __:=PRESERVE_CFG_EFFECT;
  449. __:=CIH; __:=ge; __:=e; __:=s; __:=MCFG;
  450. __:=f; __:=l; __:=i; __:=p; __:=m}
  451. | FRCallVoid f l p =>
  452. ?X1393@{__:=cfgp; __:=PRESERVE_CFG_EFFECT;
  453. __:=CIH; __:=ge; __:=e; __:=s; __:=MCFG;
  454. __:=f; __:=l; __:=p; __:=m}
  455. end
  456. | IRResumeFunction pc0 =>
  457. ?X1363@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH;
  458. __:=ge; __:=e; __:=s; __:=MCFG; __:=pc0;
  459. __:=m}
  460. end matchM)" not in guarded form (should be a
  461. constructor, an abstraction, a match, a cofix or a recursive
  462. call).
  463. Recursive definition is:
  464. "fun (ge : genv) (e : env) (s : stack) (MCFG : mcfg)
  465. (r : InterpreterResult) (m : M.memory) =>
  466. (fun
  467. lemma : M.memEffect m (step_sem_tiered ge e s MCFG r) =
  468. idM (M.memEffect m (step_sem_tiered ge e s MCFG r)) =>
  469. reflexive_proper Classes.equiv
  470. (M.memEffect m (step_sem_tiered ge e s MCFG r))
  471. (idM (M.memEffect m (step_sem_tiered ge e s MCFG r))) lemma
  472. (M.memEffect m (step_sem_tiered ge e s (monomap cfgp MCFG) r))
  473. (M.memEffect m (step_sem_tiered ge e s (monomap cfgp MCFG) r))
  474. (eq_proper_proxy
  475. (M.memEffect m (step_sem_tiered ge e s (monomap cfgp MCFG) r))))
  476. matchM
  477. (eq_ind_r
  478. (Classes.equiv (idM (M.memEffect m (step_sem_tiered ge e s MCFG r))))
  479. match
  480. r as i
  481. return
  482. (match
  483. match
  484. match i with
  485. | IRDone v => Ret (Event:=IO.IO) v
  486. | IREnterFunction _ _ =>
  487. bindM (execInterpreter ge e s MCFG i)
  488. (fun rnext : InterpreterResult =>
  489. step_sem_tiered ge e s MCFG rnext)
  490. | IRReturnFunction _ =>
  491. bindM (execInterpreter ge e s MCFG i)
  492. (fun rnext : InterpreterResult =>
  493. step_sem_tiered ge e s MCFG rnext)
  494. | IRResumeFunction _ =>
  495. bindM (execInterpreter ge e s MCFG i)
  496. (fun rnext : InterpreterResult =>
  497. step_sem_tiered ge e s MCFG rnext)
  498. end
  499. with
  500. | Ret x => Ret (Event:=IO.IO) (m, x)
  501. | @Vis _ _ Y io k =>
  502. match M.mem_step io m with
  503. | inl _ =>
  504. Err (Event:=IO.IO) (X:=M.memory * dvalue)
  505. "uninterpretiable IO call "
  506. | inr (m', v) => Trace.Tau (M.memEffect m' (k v))
  507. end
  508. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  509. | Err e0 => Err (Event:=IO.IO) (X:=M.memory * dvalue) e0
  510. end
  511. with
  512. | Ret x => Ret x
  513. | @Vis _ _ Y e0 k => Vis e0 k
  514. | Trace.Tau k => Trace.Tau k
  515. | Err s0 => Err s0
  516. end
  517. ≡ match
  518. match
  519. match i with
  520. | IRDone v => Ret (Event:=IO.IO) v
  521. | IREnterFunction _ _ =>
  522. bindM (execInterpreter ge e s (monomap cfgp MCFG) i)
  523. (fun rnext : InterpreterResult =>
  524. step_sem_tiered ge e s (monomap cfgp MCFG) rnext)
  525. | IRReturnFunction _ =>
  526. bindM (execInterpreter ge e s (monomap cfgp MCFG) i)
  527. (fun rnext : InterpreterResult =>
  528. step_sem_tiered ge e s (monomap cfgp MCFG) rnext)
  529. | IRResumeFunction _ =>
  530. bindM (execInterpreter ge e s (monomap cfgp MCFG) i)
  531. (fun rnext : InterpreterResult =>
  532. step_sem_tiered ge e s (monomap cfgp MCFG) rnext)
  533. end
  534. with
  535. | Ret x => Ret (Event:=IO.IO) (m, x)
  536. | @Vis _ _ Y io k =>
  537. match M.mem_step io m with
  538. | inl _ =>
  539. Err (Event:=IO.IO) (X:=M.memory * dvalue)
  540. "uninterpretiable IO call "
  541. | inr (m', v) => Trace.Tau (M.memEffect m' (k v))
  542. end
  543. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  544. | Err e0 => Err (Event:=IO.IO) (X:=M.memory * dvalue) e0
  545. end
  546. with
  547. | Ret x => Ret x
  548. | @Vis _ _ Y e0 k => Vis e0 k
  549. | Trace.Tau k => Trace.Tau k
  550. | Err s0 => Err s0
  551. end)
  552. with
  553. | IRDone v => EquivRet
  554. | IREnterFunction fnid args =>
  555. ?X1361@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH; __:=ge; __:=e;
  556. __:=s; __:=MCFG; __:=fnid; __:=args; __:=m}
  557. | IRReturnFunction fres =>
  558. match
  559. fres as f
  560. return
  561. (match
  562. match
  563. match
  564. execInterpreter ge e s MCFG (IRReturnFunction f)
  565. with
  566. | Ret x => Trace.Tau (step_sem_tiered ge e s MCFG x)
  567. | @Vis _ _ Y e0 k =>
  568. Vis e0
  569. (fun y : Y =>
  570. (cofix go (s0 : M IO.IO InterpreterResult) :
  571. M IO.IO dvalue :=
  572. match s0 with
  573. | Ret x =>
  574. Trace.Tau (step_sem_tiered ge e s MCFG x)
  575. | @Vis _ _ Y0 e1 k0 =>
  576. Vis e1 (fun y0 : Y0 => go (k0 y0))
  577. | Trace.Tau k0 => Trace.Tau (go k0)
  578. | Err s1 => Err (Event:=IO.IO) (X:=dvalue) s1
  579. end) (k y))
  580. | Trace.Tau k =>
  581. Trace.Tau
  582. ((cofix go (s0 : M IO.IO InterpreterResult) :
  583. M IO.IO dvalue :=
  584. match s0 with
  585. | Ret x =>
  586. Trace.Tau (step_sem_tiered ge e s MCFG x)
  587. | @Vis _ _ Y e0 k0 =>
  588. Vis e0 (fun y : Y => go (k0 y))
  589. | Trace.Tau k0 => Trace.Tau (go k0)
  590. | Err s1 => Err (Event:=IO.IO) (X:=dvalue) s1
  591. end) k)
  592. | Err s0 => Err (Event:=IO.IO) (X:=dvalue) s0
  593. end
  594. with
  595. | Ret x => Ret (Event:=IO.IO) (m, x)
  596. | @Vis _ _ Y io k =>
  597. match M.mem_step io m with
  598. | inl _ =>
  599. Err (Event:=IO.IO) (X:=M.memory * dvalue)
  600. "uninterpretiable IO call "
  601. | inr (m', v) => Trace.Tau (M.memEffect m' (k v))
  602. end
  603. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  604. | Err e0 => Err (Event:=IO.IO) (X:=M.memory * dvalue) e0
  605. end
  606. with
  607. | Ret x => Ret x
  608. | @Vis _ _ Y e0 k => Vis e0 k
  609. | Trace.Tau k => Trace.Tau k
  610. | Err s0 => Err s0
  611. end
  612. ≡ match
  613. match
  614. match
  615. execInterpreter ge e s (monomap cfgp MCFG)
  616. (IRReturnFunction f)
  617. with
  618. | Ret x =>
  619. Trace.Tau
  620. (step_sem_tiered ge e s (monomap cfgp MCFG) x)
  621. | @Vis _ _ Y e0 k =>
  622. Vis e0
  623. (fun y : Y =>
  624. (cofix go (s0 : M IO.IO InterpreterResult) :
  625. M IO.IO dvalue :=
  626. match s0 with
  627. | Ret x =>
  628. Trace.Tau
  629. (step_sem_tiered ge e s
  630. (monomap cfgp MCFG) x)
  631. | @Vis _ _ Y0 e1 k0 =>
  632. Vis e1 (fun y0 : Y0 => go (k0 y0))
  633. | Trace.Tau k0 => Trace.Tau (go k0)
  634. | Err s1 => Err (Event:=IO.IO) (X:=dvalue) s1
  635. end) (k y))
  636. | Trace.Tau k =>
  637. Trace.Tau
  638. ((cofix go (s0 : M IO.IO InterpreterResult) :
  639. M IO.IO dvalue :=
  640. match s0 with
  641. | Ret x =>
  642. Trace.Tau
  643. (step_sem_tiered ge e s
  644. (monomap cfgp MCFG) x)
  645. | @Vis _ _ Y e0 k0 =>
  646. Vis e0 (fun y : Y => go (k0 y))
  647. | Trace.Tau k0 => Trace.Tau (go k0)
  648. | Err s1 => Err (Event:=IO.IO) (X:=dvalue) s1
  649. end) k)
  650. | Err s0 => Err (Event:=IO.IO) (X:=dvalue) s0
  651. end
  652. with
  653. | Ret x => Ret (Event:=IO.IO) (m, x)
  654. | @Vis _ _ Y io k =>
  655. match M.mem_step io m with
  656. | inl _ =>
  657. Err (Event:=IO.IO) (X:=M.memory * dvalue)
  658. "uninterpretiable IO call "
  659. | inr (m', v) => Trace.Tau (M.memEffect m' (k v))
  660. end
  661. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  662. | Err e0 => Err (Event:=IO.IO) (X:=M.memory * dvalue) e0
  663. end
  664. with
  665. | Ret x => Ret x
  666. | @Vis _ _ Y e0 k => Vis e0 k
  667. | Trace.Tau k => Trace.Tau k
  668. | Err s0 => Err s0
  669. end)
  670. with
  671. | FRReturn d =>
  672. match
  673. s as l
  674. return
  675. (match
  676. match
  677. match
  678. execInterpreter ge e l MCFG
  679. (IRReturnFunction (FRReturn d))
  680. with
  681. | Ret x => Trace.Tau (step_sem_tiered ge e l MCFG x)
  682. | @Vis _ _ Y e0 k =>
  683. Vis e0
  684. (fun y : Y =>
  685. (cofix go (s0 : M IO.IO InterpreterResult) :
  686. M IO.IO dvalue :=
  687. match s0 with
  688. | Ret x =>
  689. Trace.Tau
  690. (step_sem_tiered ge e l MCFG x)
  691. | @Vis _ _ Y0 e1 k0 =>
  692. Vis e1 (fun y0 : Y0 => go (k0 y0))
  693. | Trace.Tau k0 => Trace.Tau (go k0)
  694. | Err s1 =>
  695. Err (Event:=IO.IO) (X:=dvalue) s1
  696. end) (k y))
  697. | Trace.Tau k =>
  698. Trace.Tau
  699. ((cofix go (s0 : M IO.IO InterpreterResult) :
  700. M IO.IO dvalue :=
  701. match s0 with
  702. | Ret x =>
  703. Trace.Tau
  704. (step_sem_tiered ge e l MCFG x)
  705. | @Vis _ _ Y e0 k0 =>
  706. Vis e0 (fun y : Y => go (k0 y))
  707. | Trace.Tau k0 => Trace.Tau (go k0)
  708. | Err s1 =>
  709. Err (Event:=IO.IO) (X:=dvalue) s1
  710. end) k)
  711. | Err s0 => Err (Event:=IO.IO) (X:=dvalue) s0
  712. end
  713. with
  714. | Ret x => Ret (Event:=IO.IO) (m, x)
  715. | @Vis _ _ Y io k =>
  716. match M.mem_step io m with
  717. | inl _ =>
  718. Err (Event:=IO.IO) (X:=
  719. M.memory * dvalue) "uninterpretiable IO call "
  720. | inr (m', v) => Trace.Tau (M.memEffect m' (k v))
  721. end
  722. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  723. | Err e0 => Err (Event:=IO.IO) (X:=M.memory * dvalue) e0
  724. end
  725. with
  726. | Ret x => Ret x
  727. | @Vis _ _ Y e0 k => Vis e0 k
  728. | Trace.Tau k => Trace.Tau k
  729. | Err s0 => Err s0
  730. end
  731. ≡ match
  732. match
  733. match
  734. execInterpreter ge e l (monomap cfgp MCFG)
  735. (IRReturnFunction (FRReturn d))
  736. with
  737. | Ret x =>
  738. Trace.Tau
  739. (step_sem_tiered ge e l (monomap cfgp MCFG) x)
  740. | @Vis _ _ Y e0 k =>
  741. Vis e0
  742. (fun y : Y =>
  743. (cofix go (s0 : M IO.IO InterpreterResult) :
  744. M IO.IO dvalue :=
  745. match s0 with
  746. | Ret x =>
  747. Trace.Tau
  748. (step_sem_tiered ge e l
  749. (monomap cfgp MCFG) x)
  750. | @Vis _ _ Y0 e1 k0 =>
  751. Vis e1 (fun y0 : Y0 => go (k0 y0))
  752. | Trace.Tau k0 => Trace.Tau (go k0)
  753. | Err s1 =>
  754. Err (Event:=IO.IO) (X:=dvalue) s1
  755. end) (k y))
  756. | Trace.Tau k =>
  757. Trace.Tau
  758. ((cofix go (s0 : M IO.IO InterpreterResult) :
  759. M IO.IO dvalue :=
  760. match s0 with
  761. | Ret x =>
  762. Trace.Tau
  763. (step_sem_tiered ge e l
  764. (monomap cfgp MCFG) x)
  765. | @Vis _ _ Y e0 k0 =>
  766. Vis e0 (fun y : Y => go (k0 y))
  767. | Trace.Tau k0 => Trace.Tau (go k0)
  768. | Err s1 =>
  769. Err (Event:=IO.IO) (X:=dvalue) s1
  770. end) k)
  771. | Err s0 => Err (Event:=IO.IO) (X:=dvalue) s0
  772. end
  773. with
  774. | Ret x => Ret (Event:=IO.IO) (m, x)
  775. | @Vis _ _ Y io k =>
  776. match M.mem_step io m with
  777. | inl _ =>
  778. Err (Event:=IO.IO) (X:=
  779. M.memory * dvalue)
  780. "uninterpretiable IO call "
  781. | inr (m', v) => Trace.Tau (M.memEffect m' (k v))
  782. end
  783. | Trace.Tau x' => Trace.Tau (M.memEffect m x')
  784. | Err e0 =>
  785. Err (Event:=IO.IO) (X:=M.memory * dvalue) e0
  786. end
  787. with
  788. | Ret x => Ret x
  789. | @Vis _ _ Y e0 k => Vis e0 k
  790. | Trace.Tau k => Trace.Tau k
  791. | Err s0 => Err s0
  792. end)
  793. with
  794. | [] => EquivTau (CIH ge e [] MCFG (IRDone d) m)
  795. | f :: s0 =>
  796. ?X1402@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH; __:=ge;
  797. __:=e; __:=f; __:=s0; __:=MCFG; __:=d; __:=m}
  798. end
  799. | FRReturnVoid =>
  800. ?X1391@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH; __:=ge;
  801. __:=e; __:=s; __:=MCFG; __:=m}
  802. | FRCall f l i p =>
  803. ?X1392@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH; __:=ge;
  804. __:=e; __:=s; __:=MCFG; __:=f; __:=l; __:=i; __:=p;
  805. __:=m}
  806. | FRCallVoid f l p =>
  807. ?X1393@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH; __:=ge;
  808. __:=e; __:=s; __:=MCFG; __:=f; __:=l; __:=p; __:=m}
  809. end
  810. | IRResumeFunction pc0 =>
  811. ?X1363@{__:=cfgp; __:=PRESERVE_CFG_EFFECT; __:=CIH; __:=ge; __:=e;
  812. __:=s; __:=MCFG; __:=pc0; __:=m}
  813. end matchM)".
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!