let rec decompose_up k (c, v as cv) = if k > 0 then match c with | Top -> raise Not_found | LetL (x, c', e) -> (c', (Let (x, v, e))) | AppR ((k', v'), c') -> decompose_up (k'-1) (c', App (v', v)) | AppL (c', e) -> try decompose_down (AppR ((k, v), c'), e) with Value _ -> decompose_up (k-1) (c', App (v, e)) else cv;;