Merge pull request #1110 from CakeML/efficient-cases-peg

Author: myreen

compiler/parsing/cmlPEGScript.sml

@@ -318,18 +318,22 @@ Definition cmlPEG_def[nocompute]:
                              (bindNT nE);
                         seql [tokeq CaseT; pnt nE; tokeq OfT; pnt nPEs]
                              (bindNT nE)]);
-              (mkNT nE',
-               choicel [seql [tokeq RaiseT; pnt nE'] (bindNT nE');
-                        pegf (pnt nElogicOR) (bindNT nE');
-                        seql [tokeq IfT; pnt nE; tokeq ThenT; pnt nE;
-                              tokeq ElseT; pnt nE'] (bindNT nE')]);
               (mkNT nPEs,
-               choicel [seql [pnt nPE'; tokeq BarT; pnt nPEs] (bindNT nPEs);
-                        pegf (pnt nPE) (bindNT nPEs)]);
-              (mkNT nPE, seql [pnt nPattern; tokeq DarrowT; pnt nE]
-                              (bindNT nPE));
-              (mkNT nPE', seql [pnt nPattern; tokeq DarrowT; pnt nE']
-                               (bindNT nPE'));
+               seql [pnt nPattern; tokeq DarrowT; pnt nPE] (bindNT nPEs));
+              (mkNT nPE,
+               choicel [seql [tokeq IfT; pnt nE; tokeq ThenT; pnt nE;
+                              tokeq ElseT; pnt nPE]
+                             (bindNT nPE);
+                        seql [tokeq CaseT; pnt nE; tokeq OfT; pnt nPEs]
+                             (bindNT nPE);
+                        seql [tokeq FnT; pnt nPattern; tokeq DarrowT; pnt nE]
+                             (bindNT nPE);
+                        seql [tokeq RaiseT; pnt nPE] (bindNT nPE);
+                        seql [pnt nElogicOR; pnt nPEsfx] (bindNT nPE)]);
+              (mkNT nPEsfx,
+               choicel [seql [tokeq HandleT; pnt nPEs] (bindNT nPEsfx);
+                        seql [tokeq BarT; pnt nPEs] (bindNT nPEsfx);
+                        pegf (empty []) (bindNT nPEsfx)]);
               (mkNT nAndFDecls,
                peg_linfix (mkNT nAndFDecls) (pnt nFDecl) (tokeq AndT));
               (mkNT nFDecl,
@@ -704,7 +708,7 @@ val npeg0_rwts =
                 “nEmult”, “nEadd”, “nElistop”, “nErel”, “nEcomp”,
                 “nEbefore”,
                 “nEtyped”, “nElogicAND”, “nElogicOR”, “nEhandle”,
-                “nE”, “nE'”, “nElist1”,
+                “nE”, “nPE”, “nPEs”, “nElist1”,
                 “nSpecLine”
                ]
 
@@ -732,14 +736,14 @@ val topo_nts = [“nV”, “nTyvarN”, “nTypeDec”, “nTypeAbbrevDec”,
                 “nTbase”, “nPTbase”, “nTbaseList”, “nDType”, “nPType”,
                 “nListOps”, “nRelOps”, “nPtuple”, “nPbase”, “nPapp”,
                 “nPcons”, “nPas”, “nPattern”,
-                “nPatternList”, “nPbaseList1”, “nPE”,
-                “nPE'”, “nPEs”, “nMultOps”, “nLetDec”, “nLetDecs”,
+                “nPatternList”, “nPbaseList1”,
+                “nPEs”, “nMultOps”, “nLetDec”, “nLetDecs”,
                 “nFQV”,
                 “nFDecl”, “nAddOps”, “nCompOps”, “nOpID”,
                 “nEliteral”, “nEbase”, “nEapp”,
                 “nEmult”, “nEadd”, “nElistop”, “nErel”,
                 “nEcomp”, “nEbefore”, “nEtyped”, “nElogicAND”,
-                “nElogicOR”, “nEhandle”, “nE”, “nE'”,
+                “nElogicOR”, “nPE”, “nPEsfx”, “nEhandle”, “nE”,
                 “nType”, “nTypeList1”, “nTypeList2”,
                 “nEseq”, “nElist1”, “nDtypeDecl”,
                 “nOptTypEqn”,

compiler/parsing/proofs/cmlNTPropsScript.sml

@@ -561,29 +561,6 @@ Proof
   simp[Once EXTENSION, EQ_IMP_THM] >> dsimp[]
 QED
 
-Theorem firstSet_nE':
-  firstSet cmlG (NT(mkNT nE')::rest) =
-  firstSet cmlG [NT (mkNT nEbase)] ∪ {IfT; RaiseT}
-Proof
-  simp[SimpLHS, firstSetML_eqn] >>
-  ntac 2 (simp[Once firstSetML_def, cmlG_applied, cmlG_FDOM]) >>
-  simp[Once EXTENSION, EQ_IMP_THM] >> dsimp[]
-QED
-
-Theorem firstSetML_nE'[simp]:
-  mkNT nConstructorName ∉ sn ∧ mkNT nUQConstructorName ∉ sn ∧
-  mkNT nEbase ∉ sn ∧ mkNT nFQV ∉ sn ∧ mkNT nV ∉ sn ∧ mkNT nEapp ∉ sn ∧
-  mkNT nEmult ∉ sn ∧ mkNT nEadd ∉ sn ∧ mkNT nErel ∉ sn ∧ mkNT nEcomp ∉ sn ∧
-  mkNT nEbefore ∉ sn ∧ mkNT nEtyped ∉ sn ∧ mkNT nElogicAND ∉ sn ∧
-  mkNT nElogicOR ∉ sn ∧ mkNT nE' ∉ sn ∧ mkNT nElistop ∉ sn ∧
-  mkNT nEliteral ∉ sn
-  ⇒
-  firstSetML cmlG sn (NT (mkNT nE')::rest) = firstSet cmlG [NN nE']
-Proof
-  ntac 2 (simp[Once firstSetML_def, cmlG_applied, cmlG_FDOM, firstSet_nE']) >>
-  simp[Once EXTENSION, EQ_IMP_THM] >> dsimp[]
-QED
-
 Theorem firstSet_nElist1[simp]:
   firstSet cmlG (NT (mkNT nElist1)::rest) = firstSet cmlG [NT (mkNT nE)]
 Proof
@@ -721,6 +698,14 @@ Proof
   simp[SimpLHS, Once firstSet_NT, cmlG_FDOM, cmlG_applied] >> simp[]
 QED
 
+Theorem firstSet_nPEsfx[simp]:
+  firstSet cmlG (NN nPEsfx :: rest) =
+  BarT INSERT HandleT INSERT firstSet cmlG rest
+Proof
+  simp[SimpLHS, Once firstSet_NT, cmlG_FDOM, cmlG_applied,
+       nullable_PEsfx] >> SET_TAC[]
+QED
+
 Theorem NOTIN_firstSet_nV[simp]:
   CommaT ∉ firstSet cmlG [NN nV] ∧ LparT ∉ firstSet cmlG [NN nV] ∧
   RparT ∉ firstSet cmlG [NN nV] ∧ UnderbarT ∉ firstSet cmlG [NN nV] ∧
@@ -750,7 +735,8 @@ Theorem NOTIN_firstSet_nV[simp]:
   TypeT ∉ firstSet cmlG [NN nV] ∧
   SemicolonT ∉ firstSet cmlG [NN nV] ∧ ColonT ∉ firstSet cmlG [NN nV] ∧
   StructureT ∉ firstSet cmlG [NN nV] ∧ WordT w ∉ firstSet cmlG [NN nV] ∧
-  SymbolT "::" ∉ firstSet cmlG [NN nV]
+  SymbolT "::" ∉ firstSet cmlG [NN nV] ∧
+  HandleT ∉ firstSet cmlG [NN nV]
 Proof
   simp[firstSet_nV] >> simp[validPrefixSym_def]
 QED
@@ -790,7 +776,8 @@ Theorem NOTIN_firstSet_nFQV[simp]:
   TypeT ∉ firstSet cmlG [NN nFQV] ∧
   UnderbarT ∉ firstSet cmlG [NN nFQV] ∧
   ValT ∉ firstSet cmlG [NN nFQV] ∧
-  WordT w ∉ firstSet cmlG [NN nFQV]
+  WordT w ∉ firstSet cmlG [NN nFQV] ∧
+  HandleT ∉ firstSet cmlG [NN nV]
 Proof
   simp[firstSet_nFQV]
 QED