1(*---------------------------------------------------------------------------*
2 * This example defines the abstract syntax for a simple ML-like language,   *
3 * and a simple mutually-recursive function for computing the variables      *
4 * in a program.  It exercises the type definition package on a mutually     *
5 * recursive concrete type.                                                  *
6 *                                                                           *
7 * The example is also a demonstration of how Holmake works. Just invoke     *
8 *                                                                           *
9 *     Holmake                                                               *
10 *                                                                           *
11 * and wait. When Holmake is done, a compiled theory corresponding to this   *
12 * file is found in MLSyntaxTheory.u{i,o}. It can be loaded into an          *
13 * interactive session by                                                    *
14 *                                                                           *
15 *    load "MLTheory";                                                       *
16 *                                                                           *
17 * Loading the theory can take a little while - about 5 seconds on my        *
18 * machine.                                                                  *
19 *                                                                           *
20 * If you are working interactively, i.e., you don't want to pay any         *
21 * attention to this Holmake stuff, do the following:                        *
22 *                                                                           *
23    app load ["bossLib", "stringTheory", "setTheory"];
24 *                                                                           *
25 * and then proceed with cut-and-paste.                                      *
26 *                                                                           *
27 *                                                                           *
28 *                                                                           *
29 *              GRAMMAR                                                      *
30 *             ---------                                                     *
31 *                                                                           *
32 *     atexp ::= <var>                                                       *
33 *             | "let" <dec> "in" <exp> "end"                                *
34 *                                                                           *
35 *     exp   ::= <atexp>                                                     *
36 *             | <exp> <atexp>                                               *
37 *             | "fn" <match>                                                *
38 *                                                                           *
39 *     match ::= <rule>                                                      *
40 *             | <rule> "|" <match>                                          *
41 *                                                                           *
42 *      rule ::= <pat> "=>" <exp>                                            *
43 *                                                                           *
44 *       dec ::= "val" <valbind>                                             *
45 *             | "local" <dec> "in" <dec> "end"                              *
46 *             | <dec> ";" <dec>                                             *
47 *                                                                           *
48 *   valbind ::= <pat> "=" <exp>                                             *
49 *             | <pat> "=" <exp> "and" <valbind>                             *
50 *             | "valrec" <valbind>                                          *
51 *                                                                           *
52 *     pat   ::= "_"  (* wildcard *)                                         *
53 *             | <var>                                                       *
54 *                                                                           *
55 *---------------------------------------------------------------------------*)
56
57
58open bossLib Theory Parse ;
59
60local open stringTheory pred_setTheory   (* Make strings and sets be present *)
61in end;
62
63val _ = new_theory "ML";
64
65
66(*---------------------------------------------------------------------------
67    Define the type of variables.
68 ---------------------------------------------------------------------------*)
69
70val _ = Datatype `var = VAR string`;
71
72
73(*---------------------------------------------------------------------------
74    Define the datatype of ML syntax trees.
75 ---------------------------------------------------------------------------*)
76
77val _ = Datatype
78        `atexp = var_exp var
79               | let_exp dec exp ;
80
81           exp = aexp    atexp
82               | app_exp exp atexp
83               | fn_exp  match ;
84
85         match = match  rule
86               | matchl rule match ;
87
88          rule = rule pat exp ;
89
90           dec = val_dec   valbind
91               | local_dec dec dec
92               | seq_dec   dec dec ;
93
94       valbind = bind  pat exp
95               | bindl pat exp valbind
96               | rec_bind valbind ;
97
98           pat = wild_pat
99               | var_pat var`;
100
101
102(*---------------------------------------------------------------------------
103      A simple collection of functions for finding the variables
104      in a program.
105 ----------------------------------------------------------------------------*)
106
107val Vars_def =
108 Define
109   `(atexpV (var_exp v)      = {v}) /\
110    (atexpV (let_exp d e)    = (decV d) UNION (expV e))
111     /\
112    (expV (aexp a)           = atexpV a) /\
113    (expV (app_exp e a)      = (expV e) UNION (atexpV a)) /\
114    (expV (fn_exp m)         = matchV m)
115     /\
116    (matchV (match r)        = ruleV r) /\
117    (matchV (matchl r mrst)  = (ruleV r) UNION (matchV mrst))
118     /\
119    (ruleV (rule p e)        = (patV p) UNION (expV e))
120     /\
121    (decV (val_dec b)        = valbindV b) /\
122    (decV (local_dec d1 d2)  = (decV d1) UNION (decV d2)) /\
123    (decV (seq_dec d1 d2)    = (decV d1) UNION (decV d2))
124     /\
125    (valbindV (bind p e)     = (patV p) UNION (expV e)) /\
126    (valbindV (bindl p e vb) = (patV p) UNION (expV e) UNION (valbindV vb)) /\
127    (valbindV (rec_bind vb)  = (valbindV vb))
128     /\
129    (patV wild_pat           = {}) /\
130    (patV (var_pat v)        = {v})`;
131
132val _ = export_theory();
133