Permalink
Browse files

Remove SML style datatype declarations from grammar

Now Haskell style declarations, e.g.,

   datatype 'a list = Nil | Cons 'a ('a list)

(only) must be used.  This also affects exception declarations, e.g.,

   exception Foo string (int -> bool)

Closes #611
  • Loading branch information...
mn200 committed Jan 30, 2019
1 parent be8c718 commit 439765649dab969418d87f5592e9091a52fa175e
@@ -385,9 +385,7 @@ val cmlPEG_def = zDefine`
peg_linfix (mkNT nDtypeCons) (pnt nDconstructor) (tokeq BarT)]
(bindNT nDtypeDecl));
(mkNT nDconstructor,
seql [pnt nUQConstructorName;
choicel [seql [tokeq OfT; pnt nType] I;
pnt nTbaseList]]
seql [pnt nUQConstructorName; pnt nTbaseList]
(bindNT nDconstructor));
(mkNT nUQConstructorName, peg_UQConstructorName);
(mkNT nConstructorName,
@@ -3793,8 +3793,7 @@ Theorem completeness
first_assum (unify_firstconj kall_tac o has_length) >>
qexists_tac ‘decls_pt1’ >> simp[] >> dsimp[EXISTS_PROD] >>
normlist >> first_x_assum irule >> simp[]))
>- (print_tac "nDconstructor" >> stdstart >> pmap_cases
>- (normlist >> first_assum (unify_firstconj kall_tac) >> simp[]) >>
>- (print_tac "nDconstructor" >> stdstart >> pmap_cases >>
rename [‘ptree_head upt = NN nUQConstructorName’,
‘real_fringe upt = MAP _ upf’,
‘ptree_head blpt = NN nTbaseList’,
@@ -717,16 +717,12 @@ Theorem peg_sound
by simp[NT_rank_def] >>
strip_tac >>
rveq >> simp[cmlG_FDOM, cmlG_applied, listTheory.APPEND_EQ_CONS,
MAP_EQ_SING] >> (* three subgoals, all with UQCons first *)
MAP_EQ_SING] >>
first_x_assum (qpat_x_assum ‘NT_rank _ < NT_rank _’ o
mp_then (Pos hd) mp_tac) >>
disch_then (first_assum o
mp_then (Pos hd) strip_assume_tac) >>
simp[] >> rveq >> dsimp[] >> csimp[] (* still three *)
>- (first_x_assum (qpat_assum ‘peg_eval _ (_, nt (mkNT nType) I) _’ o
mp_then Any mp_tac) >>
metis_tac[not_peg0_LENGTH_decreases, peg0_nUQConstructorName,
LENGTH, DECIDE``SUC x < y ⇒ x < y``, MAP]) >>
simp[] >> rveq >> dsimp[] >> csimp[] >>
first_x_assum (qpat_assum ‘peg_eval _ (_, nt (mkNT nTbaseList) I) _’o
mp_then Any mp_tac) >>
metis_tac[not_peg0_LENGTH_decreases, peg0_nUQConstructorName,
@@ -370,9 +370,9 @@ val _ = tytest "(bool * int)"
val _ = tytest "(bool list * int) * bool"
val _ = parsetest0 ``nDecl`` ``ptree_Decl`` "exception Foo"
(SOME ``Dexn locs "Foo" []``)
val _ = parsetest0 ``nDecl`` ``ptree_Decl`` "exception Bar of int"
val _ = parsetest0 ``nDecl`` ``ptree_Decl`` "exception Bar int"
(SOME ``Dexn locs "Bar" [Atapp [] (Short "int")]``)
val _ = parsetest0 ``nDecl`` ``ptree_Decl`` "exception Bar of int * int"
val _ = parsetest0 ``nDecl`` ``ptree_Decl`` "exception Bar int int"
(SOME ``Dexn locs "Bar"
[Atapp [] (Short "int");
Atapp [] (Short "int")]``);
@@ -472,9 +472,9 @@ val _ = parsetest ``nTopLevelDec`` ``ptree_TopLevelDec``
val _ = parsetest ``nTopLevelDec`` ``ptree_TopLevelDec`` "val x = 10"
val _ = parsetest ``nDecls`` elab_decls "fun f x y = x + y"
val _ = parsetest ``nDecls`` elab_decls
"datatype 'a list = Nil | Cons of 'a * 'a list \
"datatype 'a list = Nil | Cons 'a ('a list) \
\fun map f l = case l of Nil => Nil \
\ | Cons(h,t) => Cons(f h, map f t)"
\ | Cons h t => Cons(f h, map f t)"
val _ = parsetest0 “nDecl” “ptree_Decl”
"datatype 'a Tree = Lf1 | Nd ('a Tree) 'a ('a Tree) | Lf2 int"
(SOME “Dtype _ [(["'a"], "Tree",
@@ -484,7 +484,7 @@ val _ = parsetest0 “nDecl” “ptree_Decl”
Atapp [Atvar "'a"] (Short "Tree")]);
("Lf2", [Atapp [] (Short "int")])])]”)
val _ = parsetest0 “nDecl” “ptree_Decl”
"datatype 'a Tree = Lf1 | Nd of ('a Tree * 'a * 'a Tree) | Lf2 of int"
"datatype 'a Tree = Lf1 | Nd ('a Tree) 'a ('a Tree) | Lf2 int"
(SOME “Dtype _ [(["'a"], "Tree",
[("Lf1", []);
("Nd", [Atapp [Atvar "'a"] (Short "Tree");
@@ -554,11 +554,11 @@ val _ = parsetest ``nTypeName`` ``ptree_TypeName``
val _ = parsetest ``nConstructorName`` T "Cname"
val _ = parsetest ``nDconstructor`` ``ptree_Dconstructor`` "Cname"
val _ = parsetest ``nDconstructor`` ``ptree_Dconstructor``
"Cname of bool * 'a"
"Cname bool 'a"
val _ = parsetest ``nDtypeDecl`` ``ptree_DtypeDecl``
"'a foo = C of 'a | D of bool | E"
"'a foo = C 'a | D bool | E"
val _ = parsetest ``nTypeDec`` ``ptree_TypeDec``
"datatype 'a foo = C of 'a | D of bool | E and bar = F | G"
"datatype 'a foo = C 'a | D bool | E and bar = F | G"

(* expressions *)
val _ = parsetest ``nEbase`` ``ptree_Expr nEbase`` "x"
@@ -410,14 +410,9 @@ val ptree_Dconstructor_def = Define`
args <- ptree_TbaseList blist ;
return args
od
| [oft; ty_pt] =>
if tokcheck oft OfT then
OPTION_MAP detuplify (ptree_Type nType ty_pt)
else NONE
| _ => NONE;
SOME(cname, types)
od
| _ :: t => NONE
else NONE
`;

@@ -81,8 +81,7 @@ val cmlG_def = mk_grammar_def ginfo
(* type declarations *)
TypeName ::= UQTyOp | "(" TyVarList ")" UQTyOp | <TyvarT> UQTyOp ;
TyVarList ::= TyvarN | TyVarList "," TyvarN;
Dconstructor ::= UQConstructorName "of" Type
| UQConstructorName TbaseList;
Dconstructor ::= UQConstructorName TbaseList;
DtypeCons ::= Dconstructor | DtypeCons "|" Dconstructor;
DtypeDecl ::= TypeName "=" DtypeCons ;
DtypeDecls ::= DtypeDecl | DtypeDecls "and" DtypeDecl;
@@ -554,17 +554,17 @@ Theorem TbaseList_OK
fs[FORALL_AND_THM, DISJ_IMP_THM, MAP_EQ_APPEND] >>
metis_tac[PTbase_OK]);

Theorem Dconstructor_OK
`valid_ptree cmlG pt ∧ ptree_head pt = NN nDconstructor ∧
MAP TK toks = ptree_fringe pt ⇒
∃dc. ptree_Dconstructor pt = SOME dc`
(start >> fs[MAP_EQ_APPEND, FORALL_AND_THM, DISJ_IMP_THM] >>
rveq >> simp[ptree_Dconstructor_def, tokcheck_def]
>- (map_every (erule strip_assume_tac o n)
[UQConstructorName_OK, Type_OK] >>
simp[]) >>
Theorem Dconstructor_OK:
valid_ptree cmlG pt ∧ ptree_head pt = NN nDconstructor ∧
MAP TK toks = ptree_fringe pt
∃dc. ptree_Dconstructor pt = SOME dc
Proof
start >> fs[MAP_EQ_APPEND, FORALL_AND_THM, DISJ_IMP_THM] >>
rveq >> simp[ptree_Dconstructor_def, tokcheck_def] >>
map_every (erule strip_assume_tac o n) [UQConstructorName_OK, TbaseList_OK] >>
simp[])
simp[]
QED

Theorem DtypeCons_OK
`valid_ptree cmlG pt ∧ ptree_head pt = NN nDtypeCons ∧

0 comments on commit 4397656

Please sign in to comment.