search

au-ts / cogent

Cogent Project
https://trustworthy.systems/projects/TS/cogent.pml
Other
158 stars 26 forks source link

flatten case expressions in shallow embedding #282

Closed amosr closed 5 years ago

amosr commented 5 years ago

We can generate nicer cases. This should make the shallow embeddings a lot smaller and nicer, and fix some of the problems with code explosion in the continuation for cases.

Extended SCorres rule looks something like this:


(*
datatype ('a, 'b, 'c) X2 =
  KindOfBad "'a"|
  Restart "'b"|
  SuperGood "'c"
*)
lemma scorres_supercase_X2 :
  "scorres x x' γ ξ ⟹ 
  (⋀v v'. valRel ξ v v' ⟹ scorres ((if t1 = ''KindOfBad'' then skindofbad else if t1 = ''Restart'' then srestart else ssupergood) (shallow_tac__var v)) d1 (v'#γ) ξ) ⟹ 
  (⋀v v'. valRel ξ v v' ⟹ scorres ((if t2 = ''KindOfBad'' then skindofbad else if t2 = ''Restart'' then srestart else ssupergood) (shallow_tac__var v)) d2 (v' # VSum t2 v' # γ) ξ) ⟹ 
  (⋀v v'. valRel ξ v v' ⟹ scorres ((if t3 = ''KindOfBad'' then skindofbad else if t3 = ''Restart'' then srestart else ssupergood) (shallow_tac__var v)) d3 (v' # VSum t3 v' # VSum t3 v' # γ) ξ) ⟹ 
  scorres (case_X2 skindofbad srestart ssupergood x) (Case x' t1 d1 (Case (Var 0) t2 d2 (Let (Esac (Var 0) t3) d3))) γ ξ"
  apply (clarsimp simp: scorres_def shallow_tac__var_def valRel_X2)
  apply (erule v_sem_caseE)
   apply (cases x)
     apply fastforce
    apply fastforce
   apply fastforce

  apply (erule v_sem_caseE)
   apply (cases x; clarsimp)
     apply fastforce
    apply fastforce
   apply fastforce

  apply (erule v_sem_letE)
  apply (erule v_sem_esacE)
  apply (erule v_sem_varE)
  apply (cases x)
    apply fastforce
   apply fastforce
  apply fastforce
  done
amosr commented 5 years ago

Bilby: Shallow_Normal is a bit faster than before (11 mins instead of 14), normal proof works, scorres normal works. There are no undefineds in the shallow_normal or shallow_normal_tuples, so we could just prove tuple correspondence on top of that if we wanted to. You can still write programs that have undefineds, it's just that bilby doesn't.

amosr commented 5 years ago

New cases look something like

Cogent:

bar : X2 -> X1
bar t2 = t2
  | SuperGood t1 n1 n2 -> t1
  | KindOfBad err -> Bad
  | Restart -> Good 0 True

Shallow:

definition
  bar :: " X2⇩T ⇒  X1⇩T"
where
  "bar ds⇩0 ≡ HOL.Let ds⇩0
  (λt2. case_X2 
     (λerr. HOL.Let () (λan⇩6. HOL.Let (X1.Bad an⇩6 ::  X1⇩T) (λan⇩5. an⇩5)))
     (λds⇩4. Let⇩d⇩s ds⇩4 (λds⇩5. HOL.Let (0 :: 8 word) (λan⇩1⇩0. HOL.Let True (λan⇩1⇩1. HOL.Let (T4.make an⇩1⇩0 an⇩1⇩1) (λan⇩9. HOL.Let (X1.Good an⇩9 ::  X1⇩T) (λan⇩8. an⇩8))))))
     (λds⇩1. HOL.Let (take⇩c⇩o⇩g⇩e⇩n⇩t ds⇩1 T2.p1⇩f) (λ(t1,ds⇩3). HOL.Let (take⇩c⇩o⇩g⇩e⇩n⇩t ds⇩3 T2.p2⇩f) (λ(n1,ds⇩4). HOL.Let (take⇩c⇩o⇩g⇩e⇩n⇩t ds⇩4 T2.p3⇩f) (λ(n2,ds⇩5). t1))))
  t2)"

Note that there's only one case expression. It's not great, but it's better than it used to be. Apparently proper case syntax is too slow to parse, so we use the case_X2 fold function instead.