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