Permalink
Browse files

simplify run step cc @TiarkRompf

  • Loading branch information...
namin committed Oct 5, 2017
1 parent da1e946 commit e4222945cedfe196b49eb931eeacd6dc3d1a90d9
Showing with 2 additions and 4 deletions.
  1. +2 −4 popl18/core.rkt
@@ -73,10 +73,8 @@
(--> (in-hole M (run (code e_1) (code e_2)))
(in-hole M (reflect (code (run e_1 e_2)))) "runcc")
(--> (in-hole M (run v_1 (code e_2)))
(in-hole M (app (lam f_new x_new e_2) v_1)) "runnc"
(side-condition (not-code? (term v_1)))
(where x_new ,(variable-not-in (term (M v_1 e_2)) (term x)))
(where f_new ,(variable-not-in (term (M v_1 e_2)) (term f))))
(in-hole M e_2) "runnc"
(side-condition (not-code? (term v_1))))
(--> (in-hole P (in-hole E (reflect (code e))))
(in-hole P (letc x_new e (in-hole E (code x_new)))) "reify-reflect"
(where x_new ,(variable-not-in (term (R E e)) (term x))))

0 comments on commit e422294

Please sign in to comment.