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