get ml_pmatchTheory building (CakeML#72)

translator/ml_pmatchScript.sml

@@ -10,9 +10,9 @@ val _ = new_theory "ml_pmatch";
 val EvalPatRel_def = Define`
   EvalPatRel env a p pat ⇔
     ∀x av. a x av ⇒
-      evaluate_match F env (0,empty_store) av
+      evaluate_match F env empty_state av
         [(p,Con NONE [])] ARB
-        ((0,empty_store),
+        (empty_state,
          if ∃vars. pat vars = x
          then Rval(Conv NONE []) else Rerr(Rraise ARB))`
 
@@ -25,7 +25,7 @@ val Pmatch_def = tDefine"Pmatch"`
   (Pmatch env [Plit l] [Litv l'] =
      if l = l' then SOME env else NONE) ∧
   (Pmatch env [Pcon (SOME n) ps] [Conv (SOME (n',t')) vs] =
-     case lookup_alist_mod_env n (all_env_to_cenv env) of
+     case lookup_alist_mod_env n env.c of
       | NONE => NONE
      | SOME (l,t) =>
        if same_tid t t' ∧ LENGTH ps = l ∧
@@ -60,28 +60,30 @@ val Pmatch_cons = store_thm("Pmatch_cons",
 val Pmatch_SOME_const = store_thm("Pmatch_SOME_const",
   ``∀env ps vs env'.
       Pmatch env ps vs = SOME env' ⇒
-      all_env_to_menv env' = all_env_to_menv env ∧
-      all_env_to_cenv env' = all_env_to_cenv env``,
+      env'.m = env.m ∧
+      env'.c = env.c``,
   ho_match_mp_tac Pmatch_ind >> simp[Pmatch_def] >>
   rw[] >> BasicProvers.EVERY_CASE_TAC >> fs[] >>
-  PairCases_on`env`>>
-  fs[write_def,all_env_to_cenv_def,all_env_to_menv_def])
+  fs[write_def])
 
 val pmatch_imp_Pmatch = prove(
-  ``(∀envC s p v env.
+  ``(∀envC s p v env aenv.
       s = empty_store ⇒
-      case pmatch envC s p v env of
+      envC = aenv.c ∧ env = aenv.v ⇒
+      case pmatch envC s p v aenv.v of
       | Match env' =>
-        Pmatch (envM,envC,env) [p] [v] = SOME (envM,envC,env')
-      | _ => Pmatch (envM,envC,env) [p] [v] = NONE) ∧
-    (∀envC s ps vs env.
+        Pmatch aenv [p] [v] = SOME (aenv with v := env')
+      | _ => Pmatch aenv [p] [v] = NONE) ∧
+    (∀envC s ps vs env aenv.
       s = empty_store ⇒
-      case pmatch_list envC s ps vs env of
+      envC = aenv.c ∧ env = aenv.v ⇒
+      case pmatch_list envC s ps vs aenv.v of
       | Match env' =>
-        Pmatch (envM,envC,env) ps vs = SOME (envM,envC,env')
-      | _ => Pmatch (envM,envC,env) ps vs = NONE)``,
+        Pmatch aenv ps vs = SOME (aenv with v := env')
+      | _ => Pmatch aenv ps vs = NONE)``,
   ho_match_mp_tac pmatch_ind >>
-  rw[pmatch_def,Pmatch_def,write_def,all_env_to_cenv_def]
+  rw[pmatch_def,Pmatch_def,write_def]
+  >> TRY (rw[environment_component_equality]>>NO_TAC)
   >- (
     BasicProvers.CASE_TAC >>
     BasicProvers.CASE_TAC >>
@@ -94,10 +96,13 @@ val pmatch_imp_Pmatch = prove(
     fs[store_lookup_def] >>
     fs[empty_store_def])
   >- (
+    first_x_assum(qspec_then`aenv`mp_tac)>>simp[]>>
     BasicProvers.CASE_TAC >> fs[] >>
     simp[Once Pmatch_cons] >>
     BasicProvers.CASE_TAC >> fs[] >>
-    simp[Once Pmatch_cons] )
+    simp[Once Pmatch_cons] >> rw[Pmatch_def] >>
+    first_x_assum(qspec_then`aenv with v := a`mp_tac)>>simp[]>>
+    BasicProvers.CASE_TAC >> simp[Once Pmatch_cons])
   >- (
     Cases_on`v110`>>simp[Pmatch_def]))
   |> SIMP_RULE std_ss []
@@ -106,20 +111,19 @@ val pmatch_imp_Pmatch = prove(
 val Pmatch_imp_pmatch = store_thm("Pmatch_imp_pmatch",
   ``∀env ps vs env'.
       (Pmatch env ps vs = SOME env' ⇒
-       pmatch_list (all_env_to_cenv env) empty_store ps vs (all_env_to_env env) =
-         Match (all_env_to_env env')) ∧
+       pmatch_list env.c empty_store ps vs env.v =
+         Match env'.v) ∧
       (Pmatch env ps vs = NONE ⇒
        ∀env2.
-       pmatch_list (all_env_to_cenv env) empty_store ps vs (all_env_to_env env) ≠
+       pmatch_list env.c empty_store ps vs env.v ≠
          Match env2)``,
   ho_match_mp_tac Pmatch_ind >>
   simp[Pmatch_def,pmatch_def] >> rw[] >>
-  `∃envM envC envE. env = (envM,envC,envE)` by METIS_TAC[PAIR] >>
-  fs[all_env_to_cenv_def,all_env_to_menv_def,all_env_to_env_def,write_def] >>
+  fs[write_def] >>
   BasicProvers.CASE_TAC >> fs[] >>
   BasicProvers.EVERY_CASE_TAC >> rfs[] >> rw[] >>
   imp_res_tac Pmatch_SOME_const >>
-  fs[all_env_to_cenv_def,all_env_to_menv_def,all_env_to_env_def,write_def] >>
+  fs[write_def] >>
   rfs[] >>
   Cases_on`v20`>>fs[pmatch_def] >>
   BasicProvers.EVERY_CASE_TAC >> fs[store_lookup_def,empty_store_def])
@@ -132,14 +136,13 @@ val pmatch_PMATCH_ROW_COND_No_match = store_thm("pmatch_PMATCH_ROW_COND_No_match
   fs [PMATCH_ROW_COND_def] >>
   rw[EvalPatRel_def] >>
   first_x_assum(fn th => first_x_assum(strip_assume_tac o MATCH_MP th)) >>
-  `∃envM envC envE. env = (envM,envC,envE)` by METIS_TAC[PAIR] >> fs[] >>
-  qspecl_then[`envC`,`p`,`res`,`envE`]strip_assume_tac(CONJUNCT1 pmatch_imp_Pmatch)
-  \\ Cases_on `Pmatch (envM,envC,envE) [p] [res]` \\ fs []
-  \\ Cases_on `pmatch envC empty_store p res envE` \\ fs []
+  qspecl_then[`p`,`res`,`env`]strip_assume_tac(CONJUNCT1 pmatch_imp_Pmatch)
+  \\ Cases_on `Pmatch env [p] [res]` \\ fs []
+  \\ Cases_on `pmatch env.c empty_store p res env.v` \\ fs []
   \\ SRW_TAC [] [] \\ rw[Once evaluate_cases,PMATCH_ROW_COND_def] \\ fs []
   \\ REPEAT STRIP_TAC \\ SRW_TAC [] [] \\ rfs[]
   \\ REPEAT (POP_ASSUM MP_TAC)
-  \\ NTAC 4 (fs[Once evaluate_cases,PMATCH_ROW_COND_def]));
+  \\ NTAC 4 (fs[Once evaluate_cases,PMATCH_ROW_COND_def,empty_state_def]));
 
 val pmatch_PMATCH_ROW_COND_Match = store_thm("pmatch_PMATCH_ROW_COND_Match",
   ``EvalPatRel env a p pat ∧
@@ -148,11 +151,11 @@ val pmatch_PMATCH_ROW_COND_Match = store_thm("pmatch_PMATCH_ROW_COND_Match",
     ⇒ ∃env2. Pmatch env [p] [res] = SOME env2``,
   rw[EvalPatRel_def,PMATCH_ROW_COND_def] >>
   first_x_assum(fn th => first_x_assum(strip_assume_tac o MATCH_MP th)) >>
-  `∃envM envC envE. env = (envM,envC,envE)` by METIS_TAC[PAIR] >> fs[] >>
-  qspecl_then[`envC`,`p`,`res`,`envE`]strip_assume_tac(CONJUNCT1 pmatch_imp_Pmatch) >>
+  qspecl_then[`p`,`res`,`env`]strip_assume_tac(CONJUNCT1 pmatch_imp_Pmatch) >>
   fs[Once evaluate_cases] >> rfs[] >>
   BasicProvers.EVERY_CASE_TAC >> fs[] >>
   fs[Once evaluate_cases] >>
+  fs[empty_state_def] >>
   PROVE_TAC[]);
 
 val Eval_PMATCH_NIL = store_thm("Eval_PMATCH_NIL",
@@ -162,6 +165,8 @@ val Eval_PMATCH_NIL = store_thm("Eval_PMATCH_NIL",
       Eval env (Mat x []) (b (PMATCH xv []))``,
   rw[CONTAINER_def]);
 
+val empty_state_refs = EVAL``empty_state.refs = empty_store`` |> EQT_ELIM
+
 val Eval_PMATCH = store_thm("Eval_PMATCH",
   ``!b a x xv.
       ALL_DISTINCT (pat_bindings p []) ⇒
@@ -179,7 +184,6 @@ val Eval_PMATCH = store_thm("Eval_PMATCH",
   rw[Once evaluate_cases,PULL_EXISTS] >> fs[] >>
   first_assum(match_exists_tac o concl) >> simp[] >>
   rw[Once evaluate_cases,PULL_EXISTS] >>
-  `∃menv cenv eenv. env = (menv,cenv,eenv)` by METIS_TAC[PAIR] >> fs[] >>
   Cases_on`∃vars. PMATCH_ROW_COND pat (K T) xv vars` >> fs[] >- (
     imp_res_tac pmatch_PMATCH_ROW_COND_Match >>
     ntac 3 (pop_assum kall_tac) >>
@@ -192,7 +196,7 @@ val Eval_PMATCH = store_thm("Eval_PMATCH",
     srw_tac[DNF_ss][] >> disj1_tac >>
     imp_res_tac Pmatch_imp_pmatch >>
     imp_res_tac Pmatch_SOME_const >>
-    fs[all_env_to_cenv_def,all_env_to_env_def,pmatch_def,all_env_to_menv_def] >>
+    fs[pmatch_def] >>
     qpat_assum`X = Match Y` mp_tac >> BasicProvers.CASE_TAC >>
     fs[GSYM AND_IMP_INTRO] >>
     first_x_assum(fn th => first_assum(strip_assume_tac o MATCH_MP th)) >>
@@ -203,10 +207,10 @@ val Eval_PMATCH = store_thm("Eval_PMATCH",
     `(some x. pat x = pat vars) = SOME vars` by (
       simp[optionTheory.some_def] >>
       METIS_TAC[] ) >>
-    simp[] >> fs[all_env_to_menv_def] >> rw[] >>
-    PairCases_on`env2`>>
-    fs[all_env_to_cenv_def,all_env_to_env_def,
-       pmatch_def,all_env_to_menv_def] >>
+    simp[] >> fs[] >> rw[] >>
+    fs[pmatch_def,empty_state_refs] >>
+    rw[] >>
+    `env2 = env with v := env2.v` by rw[environment_component_equality] >>
     METIS_TAC[]) >>
   qpat_assum`evaluate F X Y (Mat A B) R`mp_tac >>
   simp[Once evaluate_cases] >> strip_tac >>
@@ -215,11 +219,12 @@ val Eval_PMATCH = store_thm("Eval_PMATCH",
   simp[PMATCH_def,PMATCH_ROW_def] >>
   imp_res_tac pmatch_PMATCH_ROW_COND_No_match >>
   imp_res_tac Pmatch_imp_pmatch >>
-  fs[all_env_to_cenv_def,all_env_to_env_def,pmatch_def] >>
-  pop_assum mp_tac >> BasicProvers.CASE_TAC >- METIS_TAC[] >>
+  fs[pmatch_def] >>
+  pop_assum mp_tac >> BasicProvers.CASE_TAC >- (
+    fs[empty_state_refs] >> METIS_TAC[] ) >>
   fs[EvalPatRel_def] >>
   first_x_assum(fn th => first_x_assum(mp_tac o MATCH_MP th)) >>
-  simp[Once evaluate_cases] >> rw[]);
+  simp[Once evaluate_cases,empty_state_refs] >> rw[]);
 
 val PMATCH_option_case_rwt = store_thm("PMATCH_option_case_rwt",
   ``((case x of NONE => NONE