1(* This example is basically the same as the one in example.sml, except
2   that the type for variables is left as a type variable.
3*)
4
5new_theory "var_ex";
6load_library_in_place (find_library "mutrec");
7
8val var_ty = (==`:'var`==)
9
10structure Ast  =
11struct
12structure TypeInfo = TypeInfo
13open TypeInfo
14val mut_rec_ty_spec =
15[{type_name = "atexp",
16
17  constructors =
18      [{name = "var_exp", arg_info = [existing var_ty]},
19       {name = "let_exp", arg_info = [being_defined "dec",
20                                      being_defined "exp"]}]},
21 {type_name = "exp",
22  constructors =
23      [{name = "aexp", arg_info = [being_defined "atexp"]},
24       {name = "app_exp", arg_info = [being_defined "exp",
25                                     being_defined "atexp"]},
26       {name = "fn_exp", arg_info = [being_defined "match"]}]},
27 {type_name = "match",
28  constructors =
29      [{name = "match", arg_info = [being_defined "rule"]},
30       {name = "match_list", arg_info = [being_defined "rule",
31                                         being_defined "match"]}]},
32 {type_name = "rule",
33  constructors =
34      [{name = "rule", arg_info = [being_defined "pat",
35                                   being_defined "exp"]}]},
36 {type_name = "dec",
37  constructors =
38      [{name = "val_dec", arg_info = [being_defined "valbind"]},
39       {name = "local_dec", arg_info = [being_defined "dec",
40                                        being_defined "dec"]},
41       {name = "seq_dec", arg_info = [being_defined "dec",
42                                      being_defined "dec"]}]},
43 {type_name = "valbind",
44  constructors =
45      [{name = "bind", arg_info = [being_defined "pat",
46                                   being_defined "exp"]},
47       {name = "bind_list", arg_info = [being_defined "pat",
48                                        being_defined "exp",
49                                        being_defined "valbind"]},
50       {name = "rec_bind", arg_info = [being_defined "valbind"]}]},
51 {type_name = "pat",
52  constructors =
53      [{name = "wild_pat", arg_info = []},
54       {name = "var_pat", arg_info = [existing var_ty]}]}];
55
56
57    val New_Ty_Existence_Thm_Name = "syntax_existence_thm"
58    val New_Ty_Induct_Thm_Name = "syntax_induction_thm"
59    val New_Ty_Uniqueness_Thm_Name = "syntax_uniqueness_thm"
60    val Constructors_Distinct_Thm_Name = "syntax_constructors_distinct"
61    val Constructors_One_One_Thm_Name = "syntax_constructors_one_one"
62    val Cases_Thm_Name = "syntax_cases"
63
64
65end; (* struct *)
66
67
68(* Prove the defining theorems for the type *)
69structure GramDef = MutRecTypeFunc (Ast);
70
71(* Just so that the constant "UNION" is defined. To actually work with sets,
72   one would want to load in the "set" library.
73*)
74val _ = new_parent "set";
75(* A simple function for finding the variables in a program *)
76
77val vars_thm = define_mutual_functions
78{name = "vars_thm", rec_axiom = syntax_existence_thm, fixities = NONE,
79 def =
80(--`(atexpV (var_exp (v:'var)) = {v}) /\
81    (atexpV (let_exp d e) = (decV d) UNION (expV e))
82     /\
83    (expV (aexp a) = atexpV a) /\
84    (expV (app_exp e a) = (expV e) UNION (atexpV a)) /\
85    (expV (fn_exp m) = matchV m)
86     /\
87    (matchV (match r) = ruleV r) /\
88    (matchV (match_list r mrst) = (ruleV r) UNION (matchV mrst))
89     /\
90    (ruleV (rule p e) = (patV p) UNION (expV e))
91     /\
92    (decV (val_dec b) = valbindV b) /\
93    (decV (local_dec d1 d2) = (decV d1) UNION (decV d2)) /\
94    (decV (seq_dec d1 d2) = (decV d1) UNION (decV d2))
95     /\
96    (valbindV (bind p e) = (patV p) UNION (expV e)) /\
97    (valbindV (bind_list p e brst) = (patV p) UNION (expV e)
98                                     UNION (valbindV brst)) /\
99    (valbindV (rec_bind vb) = (valbindV vb))
100     /\
101    (patV wild_pat = {}) /\
102    (patV (var_pat v) = {v})`--)};
103