diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/recdef.ml | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index b5f13270d7..fe6402db7d 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -172,12 +172,23 @@ let rank_for_arg_list h = | x::tl -> if predicate h x then Some i else rank_aux (i+1) tl in rank_aux 0;; +let rec check_not_nested f t = + match kind_of_term t with + | App(g, _) when eq_constr f g -> + errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function") + | Var(_) when t = f -> errorlabstrm "recdef" (str "Nested recursive function are not allowed with Function") + | _ -> iter_constr (check_not_nested f) t + + + + let rec (find_call_occs : int -> int -> constr -> constr -> (constr list -> constr) * constr list list) = fun nb_arg nb_lam f expr -> match (kind_of_term expr) with App (g, args) when g = f -> if Array.length args <> nb_arg then errorlabstrm "recdef" (str "Partial application of function " ++ Printer.pr_lconstr expr ++ str " in its body is not allowed while using Function"); + Array.iter (check_not_nested f) args; (fun l -> List.hd l), [Array.to_list args] | App (g, args) -> let (largs: constr list) = Array.to_list args in |