Modified Pancake bootstrap-related files to reflect parser updates.

CakeML · Aug 23, 2023 · d1b9280 · d1b9280
1 parent 8809fa1
commit d1b9280
Show file tree

Hide file tree

Showing 2 changed files with 18 additions and 2 deletions.
diff --git a/compiler/bootstrap/translation/from_pancake32ProgScript.sml b/compiler/bootstrap/translation/from_pancake32ProgScript.sml
@@ -459,12 +459,18 @@ Definition conv_Exp_alt_def:
               OPTION_CHOICE (OPTION_CHOICE (conv_const t) (conv_var t))
                             (conv_Exp_alt t)
           | t::v4::v5 =>
-              FOLDR (λt. OPTION_MAP2 Field (conv_nat t)) (conv_Exp_alt t) (v4::v5)
+              FOLDR (λt. OPTION_MAP2 Field (conv_nat t))
+                    (OPTION_CHOICE (conv_var t) (conv_Exp_alt t)) (v4::v5)
         else if isNT nodeNT LabelNT then
           case args of
             [] => NONE
           | [t] => OPTION_MAP Label (conv_ident t)
           | t::v6::v7 => NONE
+        else if isNT nodeNT FLabelNT then
+          case args of
+            [] => NONE
+          | [t] => OPTION_MAP Label (conv_ident t)
+          | t::v6::v7 => NONE
         else if isNT nodeNT StructNT then
           case args of
             [] => NONE
@@ -600,6 +606,8 @@ Proof
       IF_CASES_TAC
       >- (fs[]>>ntac 2 (CASE_TAC>>fs[]))>>
       IF_CASES_TAC
+      >- (fs[]>>ntac 2 (CASE_TAC>>fs[]))>>
+      IF_CASES_TAC
       >- (fs[]>>ntac 6 (CASE_TAC>>fs[]))>>
       IF_CASES_TAC>>fs[]
       >- (rpt (CASE_TAC>>fs[])>>metis_tac[option_CASES])>>

diff --git a/compiler/bootstrap/translation/from_pancake64ProgScript.sml b/compiler/bootstrap/translation/from_pancake64ProgScript.sml
@@ -463,12 +463,18 @@ Definition conv_Exp_alt_def:
               OPTION_CHOICE (OPTION_CHOICE (conv_const t) (conv_var t))
                             (conv_Exp_alt t)
           | t::v4::v5 =>
-              FOLDR (λt. OPTION_MAP2 Field (conv_nat t)) (conv_Exp_alt t) (v4::v5)
+              FOLDR (λt. OPTION_MAP2 Field (conv_nat t))
+                    (OPTION_CHOICE (conv_var t) (conv_Exp_alt t)) (v4::v5)
         else if isNT nodeNT LabelNT then
           case args of
             [] => NONE
           | [t] => OPTION_MAP Label (conv_ident t)
           | t::v6::v7 => NONE
+        else if isNT nodeNT FLabelNT then
+          case args of
+            [] => NONE
+          | [t] => OPTION_MAP Label (conv_ident t)
+          | t::v6::v7 => NONE
         else if isNT nodeNT StructNT then
           case args of
             [] => NONE
@@ -604,6 +610,8 @@ Proof
       IF_CASES_TAC
       >- (fs[]>>ntac 2 (CASE_TAC>>fs[]))>>
       IF_CASES_TAC
+      >- (fs[]>>ntac 2 (CASE_TAC>>fs[]))>>
+      IF_CASES_TAC
       >- (fs[]>>ntac 6 (CASE_TAC>>fs[]))>>
       IF_CASES_TAC>>fs[]
       >- (rpt (CASE_TAC>>fs[])>>metis_tac[option_CASES])>>