Merge pull request #862 from CakeML/gh859

Allow richer nesting of declarations in grammar

compiler/bootstrap/translation/parserProgScript.sml

@@ -145,7 +145,73 @@ val _ = translate maybe_handleRef_eq
 
 val _ = translate (def_of_const ``ptree_Expr``);
 
-val _ = translate (def_of_const ``ptree_Decl``);
+val _ = translate (def_of_const ``ptree_linfix``);
+
+val _ = translate (def_of_const ``ptree_TypeDec``);
+
+val _ = def_of_const “ptree_DtypeDecl” |> translate;
+
+val def = cmlPtreeConversionTheory.ptree_SpeclineList_def
+  |> SIMP_RULE (srw_ss()) [OPTION_CHOICE_def |> DefnBase.one_line_ify NONE,
+                           OPTION_BIND_def |> DefnBase.one_line_ify NONE,
+                           OPTION_IGNORE_BIND_def |> DefnBase.one_line_ify NONE,
+                           OPTION_GUARD_def |> DefnBase.one_line_ify NONE]
+
+val res = translate def;
+
+val _ = def_of_const “ptree_SignatureValue” |> translate
+
+Triviality ptree_Decls:
+  ptree_Decls x =
+     case x of
+     | Lf t => ptree_Decls (Lf t)
+     | Nd (a1,a2) b => ptree_Decls (Nd (a1,a2) b)
+Proof
+  Cases_on ‘x’ \\ fs []
+  \\ rename [‘Nd p’] \\ PairCases_on ‘p’ \\ fs []
+QED
+
+Triviality ptree_Structure:
+  ptree_Structure x =
+     case x of
+     | Lf t => ptree_Structure (Lf t)
+     | Nd (a1,a2) b => ptree_Structure (Nd (a1,a2) b)
+Proof
+  Cases_on ‘x’ \\ fs []
+  \\ rename [‘Nd p’] \\ PairCases_on ‘p’ \\ fs []
+QED
+
+val def =
+  LIST_CONJ
+    [cmlPtreeConversionTheory.ptree_Decl_def |> CONJUNCT1 |> SPEC_ALL,
+     ptree_Decls
+     |> ONCE_REWRITE_RULE  [cmlPtreeConversionTheory.ptree_Decl_def],
+     ptree_Structure
+     |> ONCE_REWRITE_RULE  [cmlPtreeConversionTheory.ptree_Decl_def]]
+  |> SIMP_RULE (srw_ss()) [OPTION_CHOICE_def |> DefnBase.one_line_ify NONE,
+                           OPTION_BIND_def |> DefnBase.one_line_ify NONE,
+                           OPTION_IGNORE_BIND_def |> DefnBase.one_line_ify NONE,
+                           OPTION_GUARD_def |> DefnBase.one_line_ify NONE]
+
+val res = translate_no_ind def;
+
+Triviality ind_lemma:
+  ^(first is_forall (hyp res))
+Proof
+  rpt gen_tac
+  \\ rpt (disch_then strip_assume_tac)
+  \\ match_mp_tac
+      (cmlPtreeConversionTheory.ptree_Decl_ind
+       |> SIMP_RULE (srw_ss()) [AllCaseEqs(),PULL_EXISTS])
+  \\ rpt conj_tac
+  \\ rpt strip_tac
+  \\ last_x_assum match_mp_tac
+  \\ fs []
+  \\ rpt strip_tac
+  \\ gvs [AllCaseEqs()]
+QED
+
+val _ = ind_lemma |> update_precondition;
 
 val _ = translate (def_of_const ``ptree_TopLevelDecs``);
 

compiler/parsing/cmlPEGScript.sml

@@ -451,7 +451,8 @@ Definition cmlPEG_def[nocompute]:
                  seql [tokeq LocalT; pnt nDecls; tokeq InT; pnt nDecls;
                        tokeq EndT] (bindNT nDecl);
                  seql [pnt nTypeDec] (bindNT nDecl);
-                 seql [pnt nTypeAbbrevDec] (bindNT nDecl)
+                 seql [pnt nTypeAbbrevDec] (bindNT nDecl);
+                 seql [pnt nStructure] (bindNT nDecl);
                ]);
               (mkNT nTypeAbbrevDec,
                seql [tokeq TypeT; pnt nTypeName; tokeq EqualsT; pnt nType]
@@ -487,20 +488,18 @@ Definition cmlPEG_def[nocompute]:
                seql [tokeq StructureT; pnt nStructName; pnt nOptionalSignatureAscription;
                      tokeq EqualsT; tokeq StructT; pnt nDecls; tokeq EndT]
                     (bindNT nStructure));
-              (mkNT nTopLevelDec,
-               pegf (choicel [pnt nStructure; pnt nDecl]) (bindNT nTopLevelDec));
               (mkNT nTopLevelDecs,
                choicel [
                  seql [pnt nE; tokeq SemicolonT; pnt nTopLevelDecs]
                       (bindNT nTopLevelDecs);
-                 seql [pnt nTopLevelDec; pnt nNonETopLevelDecs]
+                 seql [pnt nDecl; pnt nNonETopLevelDecs]
                       (bindNT nTopLevelDecs);
                  seql [tokeq SemicolonT; pnt nTopLevelDecs]
                       (bindNT nTopLevelDecs);
                  pegf (empty []) (bindNT nTopLevelDecs)]);
               (mkNT nNonETopLevelDecs,
                choicel [
-                 seql [pnt nTopLevelDec; pnt nNonETopLevelDecs]
+                 seql [pnt nDecl; pnt nNonETopLevelDecs]
                       (bindNT nNonETopLevelDecs);
                  seql [tokeq SemicolonT; pnt nTopLevelDecs]
                       (bindNT nNonETopLevelDecs);
@@ -676,7 +675,7 @@ end
 
 val npeg0_rwts =
     List.foldl pegnt []
-               [“nTypeDec”, “nTypeAbbrevDec”, “nOpID”,
+               [“nTypeDec”, “nTypeAbbrevDec”, “nOpID”, “nStructure”,
                 “nDecl”, “nV”, “nUQTyOp”,
                 “nUQConstructorName”, “nStructName”, “nConstructorName”,
                 “nTypeName”,
@@ -693,7 +692,7 @@ val npeg0_rwts =
                 “nEbefore”,
                 “nEtyped”, “nElogicAND”, “nElogicOR”, “nEhandle”,
                 “nE”, “nE'”, “nElist1”,
-                “nSpecLine”, “nStructure”, “nTopLevelDec”
+                “nSpecLine”
                ]
 
 fun wfnt(t,acc) = let
@@ -711,7 +710,10 @@ in
   th::acc
 end;
 
-val topo_nts = [“nV”, “nTyvarN”, “nTypeDec”, “nTypeAbbrevDec”, “nDecl”,
+val topo_nts = [“nV”, “nTyvarN”, “nTypeDec”, “nTypeAbbrevDec”,
+                “nSpecLine”, “nSpecLineList”, “nSignatureValue”,
+                “nStructure”,
+                “nDecl”,
                 “nUQTyOp”, “nUQConstructorName”, “nStructName”,
                 “nConstructorName”, “nTyVarList”, “nTypeName”, “nTyOp”,
                 “nTbase”, “nPTbase”, “nTbaseList”, “nDType”, “nPType”,
@@ -728,10 +730,9 @@ val topo_nts = [“nV”, “nTyvarN”, “nTypeDec”, “nTypeAbbrevDec”, 
                 “nType”, “nTypeList1”, “nTypeList2”,
                 “nEseq”, “nElist1”, “nDtypeDecl”,
                 “nOptTypEqn”,
-                “nDecls”, “nDconstructor”, “nAndFDecls”, “nSpecLine”,
-                “nSpecLineList”, “nSignatureValue”,
-                “nOptionalSignatureAscription”, “nStructure”,
-                “nTopLevelDec”, “nTopLevelDecs”, “nNonETopLevelDecs”
+                “nDecls”, “nDconstructor”, “nAndFDecls”,
+                “nOptionalSignatureAscription”,
+                “nTopLevelDecs”, “nNonETopLevelDecs”
                ]
 
 val cml_wfpeg_thm = save_thm(

compiler/parsing/proofs/cmlNTPropsScript.sml

@@ -83,17 +83,23 @@ Proof
   simp[Once firstSet_NT, cmlG_FDOM, cmlG_applied]
 QED
 
+Theorem firstSet_nStructure[simp]:
+  firstSet cmlG [NT (mkNT nStructure)] = {StructureT}
+Proof
+  simp[Once firstSet_NT, cmlG_FDOM, cmlG_applied]
+QED
+
 Theorem firstSet_nDecl[simp]:
   firstSet cmlG [NT (mkNT nDecl)] =
-  {ValT; FunT; DatatypeT;ExceptionT;TypeT;LocalT}
+  {ValT; FunT; DatatypeT;ExceptionT;TypeT;LocalT;StructureT}
 Proof
   simp[Once firstSet_NT, cmlG_FDOM, cmlG_applied,
        INSERT_UNION_EQ]
 QED
 
 Theorem firstSet_nDecls[simp]:
   firstSet cmlG [NN nDecls] =
-  {ValT; DatatypeT; FunT; SemicolonT; ExceptionT; TypeT; LocalT}
+  {ValT; DatatypeT; FunT; SemicolonT; ExceptionT; TypeT; LocalT;StructureT}
 Proof
   simp[firstSetML_eqn, Once firstSetML_def, cmlG_applied, cmlG_FDOM] >>
   simp[Once firstSetML_def, cmlG_applied, cmlG_FDOM] >>
@@ -151,20 +157,6 @@ Proof
        INSERT_UNION_EQ, INSERT_COMM, IMAGE_GSPEC1]
 QED
 
-Theorem firstSet_nStructure[simp]:
-  firstSet cmlG [NT (mkNT nStructure)] = {StructureT}
-Proof
-  simp[Once firstSet_NT, cmlG_FDOM, cmlG_applied]
-QED
-
-
-Theorem firstSet_nTopLevelDec[simp]:
-  firstSet cmlG [NT (mkNT nTopLevelDec)] =
-  {ValT; FunT; DatatypeT; StructureT; ExceptionT; TypeT; LocalT}
-Proof
-  simp[Once firstSet_NT, cmlG_FDOM, cmlG_applied, INSERT_UNION_EQ, INSERT_COMM]
-QED
-
 Theorem firstSet_nSpecLine[simp]:
   firstSet cmlG [NT (mkNT nSpecLine)] =
   {ValT; DatatypeT; TypeT; ExceptionT}

compiler/parsing/proofs/pegCompleteScript.sml

@@ -879,7 +879,7 @@ Definition stoppers_def:
   (stoppers nDecls =
      nestoppers DIFF
      ({BarT; StarT; AndT; SemicolonT; FunT; ValT; DatatypeT; OfT; ExceptionT;
-       TypeT; LocalT} ∪ {TyvarT s | T})) ∧
+       TypeT; LocalT; StructureT} ∪ {TyvarT s | T})) ∧
   (stoppers nDType = UNIV DIFF firstSet cmlG [NN nTyOp]) ∧
   (stoppers nDtypeCons =
      UNIV DIFF ({ArrowT; BarT; StarT; OfT; LparT} ∪ firstSet cmlG [NN nTyOp] ∪
@@ -1000,8 +1000,6 @@ Definition stoppers_def:
                 firstSet cmlG [NN nTyOp] ∪ {TyvarT s | T})) ∧
   (stoppers nTbaseList =
      UNIV DIFF ({LparT} ∪ firstSet cmlG [NN nTyOp] ∪ {TyvarT s | T})) ∧
-  (stoppers nTopLevelDec =
-     nestoppers DIFF ({LparT; BarT; StarT; AndT; OfT} ∪ {TyvarT s | T})) ∧
   (stoppers nTopLevelDecs = ∅) ∧
   (stoppers nType = UNIV DIFF ({ArrowT; StarT} ∪ firstSet cmlG [NN nTyOp])) ∧
   (stoppers nTypeAbbrevDec =
@@ -2372,21 +2370,21 @@ Proof
           simp[stoppers_def, nestoppers_def])
       >- (dsimp[Once choicel_cons] >> disj2_tac >>
           gvs[MAP_EQ_APPEND, DISJ_IMP_THM, FORALL_AND_THM] >>
-          rename [‘ptree_head TLDpt = NN nTopLevelDec’,
+          rename [‘ptree_head Dpt = NN nDecl’,
                   ‘ptree_head NeTLDspt = NN nNonETopLevelDecs’,
-                  ‘real_fringe TLDpt = MAP _ TLDfr’,
+                  ‘real_fringe Dpt = MAP _ Dfr’,
                   ‘real_fringe NeTLDspt = MAP _ NeTLDsfr’] >>
-          ‘∃eo. peg_eval cmlPEG (TLDfr ++ NeTLDsfr ++ sfx,
-                                 nt (mkNT nTopLevelDec) I)
-                         (Success (NeTLDsfr ++ sfx) [TLDpt] eo)’
+          ‘∃eo. peg_eval cmlPEG (Dfr ++ NeTLDsfr ++ sfx,
+                                 nt (mkNT nDecl) I)
+                         (Success (NeTLDsfr ++ sfx) [Dpt] eo)’
             by (Cases_on ‘NeTLDsfr = []’
                 >- (gvs[] >>
-                    ‘NT_rank (mkNT nTopLevelDec) < NT_rank (mkNT nTopLevelDecs)’
+                    ‘NT_rank (mkNT nDecl) < NT_rank (mkNT nTopLevelDecs)’
                       by simp[NT_rank_def] >>
                     first_x_assum (pop_assum o mp_then Any irule) >>
                     gs[stoppers_def]) >>
                 ‘0 < LENGTH NeTLDsfr’ by (Cases_on ‘NeTLDsfr’ >> fs[]) >>
-                ‘LENGTH TLDfr < LENGTH TLDfr + LENGTH NeTLDsfr’ by simp[] >>
+                ‘LENGTH Dfr < LENGTH Dfr + LENGTH NeTLDsfr’ by simp[] >>
                 normlist >> first_x_assum (pop_assum o mp_then Any irule) >>
                 simp[] >>
                 Cases_on ‘NeTLDsfr’ >> gs[] >>
@@ -2395,17 +2393,17 @@ Proof
                 ‘tok1 ∈ firstSet cmlG [NN nNonETopLevelDecs]’
                    by metis_tac[rfirstSet_nonempty_fringe] >>
                 fs[stoppers_def, nestoppers_def]) >>
-          ‘0 < LENGTH (MAP (TK ## I) TLDfr)’
-            by metis_tac[rfringe_length_not_nullable, nullable_TopLevelDec] >>
+          ‘0 < LENGTH (MAP (TK ## I) Dfr)’
+            by metis_tac[rfringe_length_not_nullable, nullable_Decl] >>
           fs[] >>
-          ‘∃tok1 loc1 TLDfr0. TLDfr = (tok1,loc1) :: TLDfr0’
-              by (Cases_on ‘TLDfr’ >> fs[] >> metis_tac[pair_CASES])>>
+          ‘∃tok1 loc1 Dfr0. Dfr = (tok1,loc1) :: Dfr0’
+              by (Cases_on ‘Dfr’ >> fs[] >> metis_tac[pair_CASES])>>
           gvs[] >>
-          ‘tok1 ∈ firstSet cmlG [NN nTopLevelDec]’
+          ‘tok1 ∈ firstSet cmlG [NN nDecl]’
             by metis_tac[rfirstSet_nonempty_fringe] >>
           ‘∃fl fe.
              peg_eval cmlPEG
-                      ((tok1,loc1)::(TLDfr0 ++ NeTLDsfr ++ sfx), nt (mkNT nE) I)
+                      ((tok1,loc1)::(Dfr0 ++ NeTLDsfr ++ sfx), nt (mkNT nE) I)
                       (Failure fl fe)’
             by (irule peg_respects_firstSets >> simp[] >> gs[firstSet_nE]) >>
           dxrule_then assume_tac peg_det >>
@@ -2437,23 +2435,6 @@ Proof
           >- (Cases_on ‘sfx’ >> dsimp[seql_cons, peg_eval_tok] >>
               rename [‘h::t ≠ []’] >> Cases_on ‘h’ >> gvs[stoppers_def]) >>
           csimp[choicel_cons, peg_eval_seq_SOME]))
-  >- (print_tac "nTopLevelDec" >> simp[peg_eval_NT_SOME] >>
-      simp[cmlpeg_rules_applied, FDOM_cmlPEG] >> strip_tac >>
-      gvs[MAP_EQ_SING] >> dsimp[Once choicel_cons]
-      >- (DISJ1_TAC >> first_x_assum match_mp_tac >>
-          simp[NT_rank_def, FDOM_cmlPEG] >> gvs[stoppers_def]) >>
-      DISJ2_TAC >> simp[RIGHT_EXISTS_AND_THM, LEFT_EXISTS_AND_THM] >>
-      reverse conj_tac
-      >- (simp[choicel_cons, PULL_EXISTS] >> first_x_assum irule >>
-          gs[NT_rank_def, FDOM_cmlPEG, stoppers_def]) >>
-      ‘0 < LENGTH (MAP (TK ## I) pfx)’
-        by metis_tac [rfringe_length_not_nullable, nullable_Decl] >> fs[] >>
-      Cases_on ‘pfx’ >> fs[] >>
-      rename [‘(TK ## I) pair :: MAP _ _’] >> Cases_on ‘pair’ >> fs[] >>
-      match_mp_tac peg_respects_firstSets >>
-      simp[] >> strip_tac >> rw[] >>
-      ‘StructureT ∈ firstSet cmlG [NN nDecl]’
-        by metis_tac [rfirstSet_nonempty_fringe] >> fs[])
   >- (print_tac "nTbaseList" >> stdstart
       >- (rename [‘sfx = []’] >> Cases_on ‘sfx’ >> fs[]
           >- (dsimp[not_peg0_peg_eval_NIL_NONE, peg0_nPTbase, choicel_cons] >>
@@ -3027,14 +3008,14 @@ Proof
       simp[choicel_cons, peg_eval_tok, peg_eval_seqempty])
   >- (print_tac "nNonETopLevelDecs" >> strip_tac >>
       gvs[MAP_EQ_CONS,MAP_EQ_APPEND,DISJ_IMP_THM, FORALL_AND_THM]
-      >- (rename [‘ptree_head TLDpt = NN nTopLevelDec’,
+      >- (rename [‘ptree_head Dpt = NN nDecl’,
                   ‘ptree_head NeTLDpt = NN nNonETopLevelDecs’,
-                  ‘real_fringe TLDpt = MAP _ TLDfr’,
+                  ‘real_fringe Dpt = MAP _ Dfr’,
                   ‘real_fringe NeTLDpt = MAP _ NeTLDfr’] >>
           simp[Once peg_eval_NT_SOME, cmlpeg_rules_applied] >>
-          ‘∃eo1. peg_eval cmlPEG (TLDfr ++ NeTLDfr ++ sfx,
-                                  nt (mkNT nTopLevelDec) I)
-                          (Success (NeTLDfr ++ sfx) [TLDpt] eo1)’
+          ‘∃eo1. peg_eval cmlPEG (Dfr ++ NeTLDfr ++ sfx,
+                                  nt (mkNT nDecl) I)
+                          (Success (NeTLDfr ++ sfx) [Dpt] eo1)’
             by (Cases_on ‘NeTLDfr’
                 >- (loseC “LENGTH” >> gs[] >> first_x_assum irule >>
                     gs[NT_rank_def, stoppers_def]) >> simp[] >> normlist >>
@@ -3046,7 +3027,7 @@ Proof
           dsimp[Once choicel_cons, seql_cons_SOME] >> disj1_tac >>
           pop_assum $ irule_at Any >> simp[] >> first_x_assum irule >> simp[] >>
           drule_all
-          (MATCH_MP rfringe_length_not_nullable nullable_TopLevelDec) >> simp[])
+            (MATCH_MP rfringe_length_not_nullable nullable_Decl) >> simp[])
       >- (dsimp[Once peg_eval_NT_SOME, cmlpeg_rules_applied,
                 Once choicel_cons] >> disj2_tac >>
           simp[LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM] >>
@@ -3577,12 +3558,14 @@ Proof
   >- (print_tac "nDecl" >>
       simp[Once peg_eval_NT_SOME, cmlpeg_rules_applied] >> rw[] >>
       gvs[MAP_EQ_CONS, MAP_EQ_APPEND, DISJ_IMP_THM, FORALL_AND_THM]
-      >- (dsimp[Once choicel_cons] >> DISJ1_TAC >>
+      >- (rename [‘ptree_head pt = NN nPattern’] >>
+          dsimp[Once choicel_cons] >> DISJ1_TAC >>
           simp[seql_cons_SOME, PULL_EXISTS] >> loseRK >>
           SKTAC >> normlist >> first_assum $ irule_at Any >>
           simp[stoppers_def] >> first_x_assum $ irule_at Any >>
           gvs[stoppers_def])
-      >- (dsimp[Ntimes choicel_cons 2, seql_cons_SOME] >>
+      >- (rename [‘ptree_head afdpt = NN nAndFDecls’] >>
+          dsimp[Ntimes choicel_cons 2, seql_cons_SOME] >>
           gvs[seql_cons, peg_eval_tok, stoppers_def, nestoppers_def]) >~
       [‘ptree_head tpt = NN nTypeDec’]
       >- (drule_all (MATCH_MP rfringe_length_not_nullable nullable_TypeDec) >>
@@ -3613,7 +3596,15 @@ Proof
           simp[seql_cons_SOME, PULL_EXISTS] >> loseRK >> SKTAC >>
           normlist >> first_assum $ irule_at Any >>
           simp[stoppers_def, nestoppers_def] >>
-          first_x_assum $ irule_at Any >> gvs[stoppers_def, nestoppers_def]))
+          first_x_assum $ irule_at Any >> gvs[stoppers_def, nestoppers_def]) >>
+      rename [‘ptree_head spt = NN nStructure’] >>
+      drule_all
+        (MATCH_MP rfringe_length_not_nullable nullable_Structure) >>
+      simp[] >> Cases_on ‘pfx’ >> gvs[PAIR_MAP] >>
+      drule_all rfirstSet_nonempty_fringe >> simp[PULL_EXISTS] >> rw[] >>
+      gvs[] >>
+      simp[choicel_cons, seql_cons, peg_eval_tok, peg_respects_firstSets_rwt] >>
+      dsimp[] >> first_x_assum irule >> simp[NT_rank_def, stoppers_def])
   >- (print_tac "nDconstructor" >> stdstart >>
       rename [‘ptree_head upt = NN nUQConstructorName’,
               ‘real_fringe upt = MAP _ upf’,