Permalink
Browse files

Merge pull request #613 from CakeML/gh611

Remove SML style datatype declarations from grammar
  • Loading branch information...
xrchz committed Feb 4, 2019
2 parents 2d7c75f + 1088d0f commit 0b669f77530f96dc7e085265545c193a6cd256f2
Showing with 53 additions and 70 deletions.
  1. +2 −2 characteristic/examples/cf_examplesScript.sml
  2. +1 −1 compiler/benchmarks/cakeml_benchmarks/cakeml/btree.sml
  3. +1 −1 compiler/benchmarks/cakeml_benchmarks/cakeml/queue.sml
  4. +4 −4 compiler/benchmarks/cakeml_benchmarks/cakeml/sptree_contain.sml
  5. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/even-odd.sml
  6. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/fib.sml
  7. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/imp-for.sml
  8. +2 −4 compiler/benchmarks/mlton_benchmarks/cakeml/knuth-bendix.sml
  9. +2 −2 compiler/benchmarks/mlton_benchmarks/cakeml/life.sml
  10. +5 −5 compiler/benchmarks/mlton_benchmarks/cakeml/logic.sml
  11. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/merge.sml
  12. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/pidigits.sml
  13. +4 −6 compiler/benchmarks/mlton_benchmarks/cakeml/ratio-regions.sml
  14. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/smith-normal-form.sml
  15. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/tailfib.sml
  16. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/vector-concat.sml
  17. +1 −1 compiler/benchmarks/mlton_benchmarks/cakeml/vector-rev.sml
  18. +1 −3 compiler/parsing/cmlPEGScript.sml
  19. +1 −2 compiler/parsing/proofs/pegCompleteScript.sml
  20. +2 −6 compiler/parsing/proofs/pegSoundScript.sml
  21. +8 −8 compiler/parsing/tests/cmlTestsScript.sml
  22. +0 −5 semantics/cmlPtreeConversionScript.sml
  23. +1 −2 semantics/gramScript.sml
  24. +10 −10 semantics/proofs/cmlPtreeConversionPropsScript.sml
@@ -206,7 +206,7 @@ val example_raise_spec = Q.prove (
);

val example_handle = process_topdecs
`exception Foo of int
`exception Foo int
fun example_handle x = (raise (Foo 3)) handle Foo i => i`
(* handle precedence bug in the parser? *)

@@ -231,7 +231,7 @@ val example_handle_spec = Q.prove (
);

val example_handle2 = process_topdecs
`exception Foo of int
`exception Foo int
fun example_handle2 x =
(if x > 0 then
1
@@ -1,5 +1,5 @@
datatype tree = Leaf
| Branch of tree * int * tree;
| Branch tree int tree;
fun insert x t =
case t
of Leaf => (Branch Leaf x Leaf)
@@ -1,4 +1,4 @@
datatype 'a q = QUEUE of 'a list * 'a list;
datatype 'a q = QUEUE ('a list) ('a list);
val empty = QUEUE [] [];
fun is_empty q =
case q
@@ -3,10 +3,10 @@

val with_inserts = True

datatype 'a sptree_spt = Bs of 'a sptree_spt * 'a * 'a sptree_spt
| Bn of 'a sptree_spt * 'a sptree_spt
| Ls of 'a
| Ln;
datatype 'a sptree_spt = Bs ('a sptree_spt) 'a ('a sptree_spt)
| Bn ('a sptree_spt) ('a sptree_spt)
| Ls 'a
| Ln;

fun lookup v7 v8 =
case v8
@@ -1,5 +1,5 @@
fun abs i = if i < 0 then ~i else i
exception Fail of string
exception Fail string

fun even' i = case i of
0 => True
@@ -1,4 +1,4 @@
exception Fail of string;
exception Fail string;

fun fib n =
case n of
@@ -1,4 +1,4 @@
exception Fail of string;
exception Fail string;

fun for start stop f
= let
@@ -45,7 +45,7 @@ structure Main =

(******* Quelques definitions du prelude CAML **************)

exception Failure of string;
exception Failure string;

fun failwith s = raise(Failure s)

@@ -153,9 +153,7 @@ fun union l1 =

(****************** Term manipulations *****************)

datatype term
= Var of int
| Term of string * term list
datatype term = Var int | Term string (term list)

fun vars t = case t of
(Var n) => [n]
@@ -5,7 +5,7 @@ structure Main =
[] => []
| (a::x) => f a :: map f x

exception Ex_undefined of string
exception Ex_undefined string
fun error str = raise Ex_undefined str

fun accumulate f = let
@@ -74,7 +74,7 @@ structure Main =
and diff x y = filter (fn x => not (member y x)) x
in f [] [] [] [] x end

datatype generation = GEN of (int*int) list
datatype generation = GEN ((int*int) list)
fun alive (GEN livecoords) = livecoords
and mkgen coordlist = GEN (lexordset coordlist)
and mk_nextgen_fn neighbours gen =
@@ -5,12 +5,12 @@
structure Term =
struct
datatype term
= STR of string * term list
| INT of int
| CON of string
| REF of term option ref
= STR string (term list)
| INT int
| CON string
| REF (term option ref)

exception BadArg of string
exception BadArg string
end;

(* trail.sml *)
@@ -1,5 +1,5 @@
(* Written by Stephen Weeks (sweeks@sweeks.com). *)
exception Fail of string;
exception Fail string;

fun merge (l1: int list, l2) =
case (l1, l2) of
@@ -2,7 +2,7 @@ fun print _ = ()

structure Stream =
struct
datatype 'a u = Nil | Cons of 'a * (unit -> 'a u)
datatype 'a u = Nil | Cons 'a (unit -> 'a u)
type 'a t = unit -> 'a u

fun unfold f =
@@ -15,7 +15,7 @@
*)
fun print _ = ()

exception Fail of string
exception Fail string


fun doo(max: int, f: int -> unit) =
@@ -76,7 +76,7 @@ fun some_vector(v, p) =
fun x(x, _) = x
fun y(_, y) = y

datatype 'a matrix = Matrix of 'a array array
datatype 'a matrix = Matrix ('a array array)

fun make_matrix(m: int, n: int, a) =
Matrix(map_n_vector(m, fn i => make_vector(n, a)))
@@ -86,9 +86,7 @@ fun matrix_columns(Matrix a) = vector_length(vector_ref(a, 0))
fun matrix_ref(Matrix a, i, j) = vector_ref(vector_ref(a, i), j)
fun matrix_set(Matrix a, i, j, x) = vector_set(vector_ref(a, i), j, x)

datatype pormatValue =
Int of int
| String of string
datatype pormatValue = Int int | String string

fun pormat(control_string: string, values: pormatValue list) =
let
@@ -170,7 +168,7 @@ fun positive_plus(x, y) = if negative x then x else x + y

datatype 'a queue =
Nil
| Cons of 'a * 'a queue ref
| Cons 'a ('a queue ref)

fun rao_ratio_region(c_right, c_down, w, lg_max_v) =
let val height = matrix_rows w
@@ -356,7 +356,7 @@ val table = [[ 8, ~3, 1, 3, 6, 9, ~2, 4, ~9, ~9, 2, 3, 8, ~

fun f (x, y) = List.nth (List.nth table x) y
fun show m = print (Matrix.toString (m, Int.toString))
exception Fail of string;
exception Fail string;
structure Main =
struct
fun snf() =
@@ -1,4 +1,4 @@
exception Fail of string;
exception Fail string;

fun fib' n a b = case n of
0 => a
@@ -1,5 +1,5 @@
(* Written by Stephen Weeks (sweeks@sweeks.com). *)
exception Fail of string;
exception Fail string;

structure Main =
struct
@@ -1,5 +1,5 @@
(* Written by Stephen Weeks (sweeks@sweeks.com). *)
exception Fail of string;
exception Fail string;

structure Main =
struct
@@ -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 0b669f7

Please sign in to comment.