equal
deleted
inserted
replaced
96 |
96 |
97 |
97 |
98 |
98 |
99 (** check translation rules **) |
99 (** check translation rules **) |
100 |
100 |
101 (*a wellformed rule (lhs, rhs): (ast * ast) obeys the following conditions: |
|
102 - the lhs has unique vars, |
|
103 - vars of rhs is subset of vars of lhs*) |
|
104 |
|
105 fun rule_error (rule as (lhs, rhs)) = |
101 fun rule_error (rule as (lhs, rhs)) = |
106 let |
102 let |
107 fun vars_of (Constant _) = [] |
103 fun add_vars (Constant _) = I |
108 | vars_of (Variable x) = [x] |
104 | add_vars (Variable x) = cons x |
109 | vars_of (Appl asts) = List.concat (map vars_of asts); |
105 | add_vars (Appl asts) = fold add_vars asts; |
110 |
106 |
111 fun unique (x :: xs) = not (x mem xs) andalso unique xs |
107 val lvars = add_vars lhs []; |
112 | unique [] = true; |
108 val rvars = add_vars rhs []; |
113 |
|
114 val lvars = vars_of lhs; |
|
115 val rvars = vars_of rhs; |
|
116 in |
109 in |
117 if not (unique lvars) then SOME "duplicate vars in lhs" |
110 if has_duplicates (op =) lvars then SOME "duplicate vars in lhs" |
118 else if not (rvars subset lvars) then SOME "rhs contains extra variables" |
111 else if not (rvars subset lvars) then SOME "rhs contains extra variables" |
119 else NONE |
112 else NONE |
120 end; |
113 end; |
121 |
114 |
122 |
115 |