[CakeML-Dev] CF to translator

[Ramana Kumar]

I have proved the following connection between CF's app_basic (as on
master) and a revised formulation of the translator's Arrow, modulo 4
cheats. In this email, I will show: the final theorem proved, the cheated
lemmas, and the new Arrow definition. I ask for the following feedback:
1. Does the final theorem look like a strong enough connection?
2. Do any of the cheated lemmas look false?
3. Does the Arrow definition look reasonable?.
If there aren't any problems, then I can work towards upgrading the
translator to use this definition, and proving the cheats.

Final theorem:
  |- Arrow a b f v ⇔ ∀x v1. a x v1 ⇒ app_basic p v v1 emp (cond ∘ b (f x))

Cheated lemmas:
(N.B. I want someone else to prove 2. I can tackle the rest.)

1. evaluate ck env s exp (s',r) ⇒ LENGTH s.refs ≤ LENGTH s'.refs

2. evaluate F env st exp (st',Rval res) ∧
   SPLIT (st2heap p st') (g,st2heap p st) ⇒
   st'.ffi = st.ffi

3. evaluate F env (empty_state with refs := s.refs) exp
     (empty_state with refs := s.refs ++ refs',Rval x) ⇒
   evaluate F env s exp (s with refs := s.refs ++ refs',Rval x)

(s is 'ffi state, whereas empty_state is unit state)

4. evaluate F env s es (s',Rval r) ∧ s.refs ≼ s'.refs ∧ s'.ffi = s.ffi ∧
   t = empty_state with refs := s.refs ∧
   t' = empty_state with refs := s'.refs ⇒
   evaluate F env t es (t',Rval r)

Arrow definition:
Arrow a b = (λf v. ∀x. AppReturns (a x) v (b (f x)))
AppReturns P cl Q ⇔
     ∀v.
       P v ⇒
       ∀refs.
         ∃env exp refs' u.
           do_opapp [cl; v] = SOME (env,exp) ∧
           evaluate F env (empty_state with refs := refs) exp
             (empty_state with refs := refs ++ refs',Rval u) ∧ Q u
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.cakeml.org/pipermail/developers/attachments/20161007/07fddae1/attachment.html>