127 (* Two kinds of depth measure for HOAS terms, a first order (flat) and a |
127 (* Two kinds of depth measure for HOAS terms, a first order (flat) and a |
128 higher order one. |
128 higher order one. |
129 Note: not stable of eta-contraction: embedding eta-expands term, |
129 Note: not stable of eta-contraction: embedding eta-expands term, |
130 thus we assume eta-expanded *) |
130 thus we assume eta-expanded *) |
131 fun fo_term_height (a $ b) = |
131 fun fo_term_height (a $ b) = |
132 IsaPLib.max (1 + fo_term_height b, (fo_term_height a)) |
132 Int.max (1 + fo_term_height b, (fo_term_height a)) |
133 | fo_term_height (Abs(_,_,t)) = fo_term_height t |
133 | fo_term_height (Abs(_,_,t)) = fo_term_height t |
134 | fo_term_height _ = 0; |
134 | fo_term_height _ = 0; |
135 |
135 |
136 fun ho_term_height (a $ b) = |
136 fun ho_term_height (a $ b) = |
137 1 + (IsaPLib.max (ho_term_height b, ho_term_height a)) |
137 1 + (Int.max (ho_term_height b, ho_term_height a)) |
138 | ho_term_height (Abs(_,_,t)) = ho_term_height t |
138 | ho_term_height (Abs(_,_,t)) = ho_term_height t |
139 | ho_term_height _ = 0; |
139 | ho_term_height _ = 0; |
140 |
140 |
141 |
141 |
142 (* Higher order matching with exception handled *) |
142 (* Higher order matching with exception handled *) |