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.
5 *---------------------------------------------------------------------------*)
6
7app load ["mutrecLib", "stringTheory", "setTheory"];
8
9
10(*---------------------------------------------------------------------------
11 * First, we define a type of variables.
12 *---------------------------------------------------------------------------*)
13
14val var_Axiom =
15  Define_type.define_type
16     {name="var_Axiom",
17      fixities = [Term.Prefix],
18      type_spec =`var = VAR of string`};
19
20val var_ty = Parse.Type`:var`;
21
22
23(*------------GRAMMAR---------------------------------------------------------
24
25       atexp ::= <var>
26               | let <dec> in <exp> end
27
28       exp   ::= <atexp>
29               | <exp> <atexp>
30               | fn <match>
31
32       match ::= <rule>
33               | <rule> "|" <match>
34
35       rule ::= <pat> => <exp>
36
37       dec   ::= val <valbind>
38               | local <dec> in <dec> end
39               | <dec> ; <dec>
40
41     valbind ::= <pat> = <exp>
42               | <pat> = <exp> and <valbind>
43               | valrec <valbind>
44
45       pat   ::= _  (* wildcard *)
46               | <var>
47
48 *------------------------------------------------------------------------*)
49
50local open TypeInfo
51in
52val syntax_spec =
53[{type_name = "atexp",
54  constructors =
55      [{name = "var_exp", arg_info = [existing var_ty]},
56       {name = "let_exp", arg_info = [being_defined "dec",
57                                      being_defined "exp"]}]},
58 {type_name = "exp",
59  constructors =
60      [{name = "aexp", arg_info = [being_defined "atexp"]},
61       {name = "app_exp", arg_info = [being_defined "exp",
62                                     being_defined "atexp"]},
63       {name = "fn_exp", arg_info = [being_defined "match"]}]},
64 {type_name = "match",
65  constructors =
66      [{name = "match", arg_info = [being_defined "rule"]},
67       {name = "match_list", arg_info = [being_defined "rule",
68                                         being_defined "match"]}]},
69 {type_name = "rule",
70  constructors =
71      [{name = "rule", arg_info = [being_defined "pat",
72                                   being_defined "exp"]}]},
73 {type_name = "dec",
74  constructors =
75      [{name = "val_dec", arg_info = [being_defined "valbind"]},
76       {name = "local_dec", arg_info = [being_defined "dec",
77                                        being_defined "dec"]},
78       {name = "seq_dec", arg_info = [being_defined "dec",
79                                      being_defined "dec"]}]},
80 {type_name = "valbind",
81  constructors =
82      [{name = "bind", arg_info = [being_defined "pat",
83                                   being_defined "exp"]},
84       {name = "bind_list", arg_info = [being_defined "pat",
85                                        being_defined "exp",
86                                        being_defined "valbind"]},
87       {name = "rec_bind", arg_info = [being_defined "valbind"]}]},
88 {type_name = "pat",
89  constructors =
90      [{name = "wild_pat", arg_info = []},
91       {name = "var_pat", arg_info = [existing var_ty]}]}]
92end;
93
94
95(*---------------------------------------------------------------------------
96 * Now define the type!
97 *---------------------------------------------------------------------------*)
98val {Cases = syntax_cases,
99     Constructors_Distinct = syntax_constructors_distinct,
100     Constructors_One_One = syntax_constructors_one_one,
101     New_Ty_Existence = syntax_existence_thm,
102     New_Ty_Uniqueness = syntax_uniqueness_thm,
103     New_Ty_Induct = syntax_induction_thm,
104     Argument_Extraction_Defs}
105 = Lib.time
106     mutrecLib.define_type syntax_spec;
107
108
109(*---------------------------------------------------------------------------
110 * A simple function for finding the variables in an expression of
111 * the defined syntax.
112 *---------------------------------------------------------------------------*)
113
114val vars_thm = mutrecLib.define_mutual_functions
115{name = "vars_thm", rec_axiom = syntax_existence_thm, fixities = NONE,
116 def = Parse.Term
117
118   `(atexpV (var_exp v) = {v}) /\
119    (atexpV (let_exp d e) = (decV d) UNION (expV e))
120     /\
121    (expV (aexp a) = atexpV a) /\
122    (expV (app_exp e a) = (expV e) UNION (atexpV a)) /\
123    (expV (fn_exp m) = matchV m)
124     /\
125    (matchV (match r) = ruleV r) /\
126    (matchV (match_list r mrst) = (ruleV r) UNION (matchV mrst))
127     /\
128    (ruleV (rule p e) = (patV p) UNION (expV e))
129     /\
130    (decV (val_dec b) = valbindV b) /\
131    (decV (local_dec d1 d2) = (decV d1) UNION (decV d2)) /\
132    (decV (seq_dec d1 d2) = (decV d1) UNION (decV d2))
133     /\
134    (valbindV (bind p e) = (patV p) UNION (expV e)) /\
135    (valbindV (bind_list p e brst) = (patV p) UNION (expV e)
136                                     UNION (valbindV brst)) /\
137    (valbindV (rec_bind vb) = (valbindV vb))
138     /\
139    (patV wild_pat = {}) /\
140    (patV (var_pat v) = {v})`};
141
142
143(* Warning!
144
145One has to exercise a little discipline with variable names in
146quotations that define mutually recursive functions. Type inference will
147attempt to unify the types of variables in different clauses. This is
148OK, provided that, as in the example above, all occurrences of "d" are
149to have type `:dec` (for instance). However, if one tries to have the
150clauses
151
152  (matchV (match_list r rst) = (ruleV r) UNION (matchV rst))
153
154and
155
156  (valbindV (bind_list p e rst) = (patV p) UNION (expV e) UNION (valbindV rst))
157
158appear in the same mutually recursive function definition, type
159inference will attempt to make the types of both "rst" be the same. This
160will fail, since the first is supposed to have the type `:match` and the
161second `:valbind`.
162
163This is _not_ a bug in type inference, but a shortcoming in the form that
164an input term may have; something should be done to allow the
165restriction of scope of variables in the term that specifies the
166function (like allowing quantification for each conjunct).
167*)
168