158 exception SAME; |
158 exception SAME; |
159 |
159 |
160 fun norm_term1 (asol,t) : term = |
160 fun norm_term1 (asol,t) : term = |
161 let fun norm (Var (w,T)) = |
161 let fun norm (Var (w,T)) = |
162 (case xsearch(asol,w) of |
162 (case xsearch(asol,w) of |
163 Some u => normh u |
163 Some u => (norm u handle SAME => u) |
164 | None => raise SAME) |
164 | None => raise SAME) |
165 | norm (Abs(a,T,body)) = Abs(a, T, norm body) |
165 | norm (Abs(a,T,body)) = Abs(a, T, norm body) |
166 | norm (Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) |
166 | norm (Abs(_,_,body) $ t) = normh(subst_bound (t, body)) |
167 | norm (f $ t) = |
167 | norm (f $ t) = |
168 ((case norm f of |
168 ((case norm f of |
169 Abs(_,_,body) => normh(subst_bounds([t], body)) |
169 Abs(_,_,body) => normh(subst_bound (t, body)) |
170 | nf => nf $ normh t) |
170 | nf => nf $ (norm t handle SAME => t)) |
171 handle SAME => f $ norm t) |
171 handle SAME => f $ norm t) |
172 | norm _ = raise SAME |
172 | norm _ = raise SAME |
173 and normh t = (norm t) handle SAME => t |
173 and normh t = norm t handle SAME => t |
174 in normh t end |
174 in normh t end |
175 |
175 |
176 and norm_term2(asol,iTs,t) : term = |
176 and norm_term2(asol,iTs,t) : term = |
177 let fun normT(Type(a,Ts)) = Type(a, normTs Ts) |
177 let fun normT(Type(a,Ts)) = Type(a, normTs Ts) |
178 | normT(TFree _) = raise SAME |
178 | normT(TFree _) = raise SAME |
189 (case xsearch(asol,w) of |
189 (case xsearch(asol,w) of |
190 Some u => normh u |
190 Some u => normh u |
191 | None => Var(w,normT T)) |
191 | None => Var(w,normT T)) |
192 | norm(Abs(a,T,body)) = |
192 | norm(Abs(a,T,body)) = |
193 (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body)) |
193 (Abs(a,normT T,normh body) handle SAME => Abs(a, T, norm body)) |
194 | norm(Abs(_,_,body) $ t) = normh(subst_bounds([t], body)) |
194 | norm(Abs(_,_,body) $ t) = normh(subst_bound (t, body)) |
195 | norm(f $ t) = |
195 | norm(f $ t) = |
196 ((case norm f of |
196 ((case norm f of |
197 Abs(_,_,body) => normh(subst_bounds([t], body)) |
197 Abs(_,_,body) => normh(subst_bound (t, body)) |
198 | nf => nf $ normh t) |
198 | nf => nf $ normh t) |
199 handle SAME => f $ norm t) |
199 handle SAME => f $ norm t) |
200 | norm _ = raise SAME |
200 | norm _ = raise SAME |
201 and normh t = (norm t) handle SAME => t |
201 and normh t = (norm t) handle SAME => t |
202 in normh t end; |
202 in normh t end; |