Fix bvl_const translation

ncough · May 2, 2018 · dace3f5 · dace3f5
1 parent a2f6548
commit dace3f5
Showing 1 changed file with 20 additions and 1 deletion.
diff --git a/compiler/bootstrap/translation/to_dataProgScript.sml b/compiler/bootstrap/translation/to_dataProgScript.sml
@@ -903,7 +903,21 @@ val bvl_inline_tick_inline_all_side = Q.prove (
   \\ once_rewrite_tac [fetch "-" "bvl_inline_tick_inline_all_side_def"] \\ fs [])
   |> update_precondition;
 
-val _ = translate (bvl_constTheory.compile_def)
+(* ------------------------------------------------------------------------- *)
+(* bvl_const (PMATCH translations)                                           *)
+(* ------------------------------------------------------------------------- *)
+
+val _ = translate bvl_constTheory.dest_simple_pmatch
+val _ = translate bvl_constTheory.case_op_const_pmatch
+val _ = translate bvl_constTheory.SmartOp_flip_pmatch
+(* val r = translate bvl_constTheory.SmartOp2_pmatch *) (* prove_EvalPatBind failed *)
+val _ = translate bvl_constTheory.SmartOp2_def
+val _ = translate bvl_constTheory.SmartOp_pmatch
+val _ = translate bvl_constTheory.extract_pmatch
+val _ = translate bvl_constTheory.extract_list_def
+val _ = translate bvl_constTheory.delete_var_pmatch
+
+val _ = translate bvl_constTheory.compile_def
 
 val bvl_const_compile_side = Q.prove(`
   ∀x y. bvl_const_compile_side x y ⇔ T`,
@@ -915,6 +929,11 @@ val bvl_const_compile_side = Q.prove(`
   rw[]>>
   simp[Once (fetch "-" "bvl_const_compile_side_def")])|>update_precondition
 
+val _ = translate bvl_constTheory.compile_exp_def
+
+(* ------------------------------------------------------------------------- *)
+(* ------------------------------------------------------------------------- *)
+
 val _ = translate(bvl_to_bviTheory.compile_int_def)
 
 val bvl_to_bvi_compile_int_side = Q.prove(`