Commits

cacol89  committed 602205f

added check for double recursive calls in a single rule

  • Participants
  • Parent commits 1edc4ad

Comments (0)

Files changed (3)

File src/rule_preproc.ml

         else false
     | _ -> false
 
-(** Given a list of rules that define a predicate, checks that there is at
- * most one recursive rule, and places it at the end. If there is any
- * negative recursion, an error is raised.*)
-let check_rec_rule rule_lst =
-    if rule_lst = [] then [] else
-    let key = symtkey_of_rule (List.hd rule_lst) in
-    let is_rec rule =
-        let body = rule_body rule in
-        let eval_lst = List.map (check_rec_term key) body in
-        List.fold_left (||) false eval_lst
+(** Returns true if the provided rule contains a call to itself.
+ * If the recursive call is negative, then an error is raised.
+ * If there is more than one recursive call to itself, an error is raised.*)
+let is_rec_rule rule =
+    let key = symtkey_of_rule rule in
+    let body = rule_body rule in
+    let rec_eval acc rule =
+        if check_rec_term key rule then acc+1 else acc
     in
+    let rec_count = List.fold_left rec_eval 0 body in
+    if rec_count > 1 then
+        raise (Yadi_error(
+            "Predicate "^(string_of_symtkey key)^
+            " has more than one recursive call"
+        ))
+    else
+        rec_count = 1
+
+(** Given a list of rules that define a predicate, checks that they
+ * satisfy the recursion conditions of YADI, which are:
+ *
+ * - There cannot be negative recursive calls.
+ * - A single rule cannot make more than one recursive call.
+ * - There is at most one recursive rule.
+ *
+ * If the conditions are satisfied and there is a recursive rule,
+ * then this recursive rule is placed at the end of the list.
+ *)
+let check_rec_rule rule_lst =
     let rec_split rule (r_lst,nr_lst) =
-        if is_rec rule then (rule::r_lst, nr_lst)
+        if is_rec_rule rule then (rule::r_lst, nr_lst)
         else (r_lst, rule::nr_lst)
     in
     (*Split the rules in recursive and not revursive*)
     let (r_lst, nr_lst) = List.fold_right rec_split rule_lst ([],[]) in
     (*Check condition and return list with recursion at the end*)
     match r_lst with
-        | _::_::_ ->
+        | hd::_::_ ->
             raise (Yadi_error (
+                let key = symtkey_of_rule hd in
                 "Predicate "^(string_of_symtkey key)^
                 " contains more than one recursive definition"
             ))
 (** Given a symtable, performs preprocess operations over the rules
  * contained in it. This operations are:
  *  - Extraction of constants in predicates
- *  - Recursion checks (only one recursive rule, and not negated)
+ *  - Recursion checks (only one recursive rule, only one recursive call,
+ *      and not negated recursions)
  *)
 let preprocess_rules (st:symtable) =
     let rep_rule key rules =

File test/expected/integration/family2.out

 
 yadi$ YADI execution error: Predicate Ancestor/2 contains more than one recursive definition
 
+yadi$ YADI execution error: Predicate Male_ancestor/2 has more than one recursive call
+
 yadi$ 

File test/integration/family2.datalog

 Ancestor(x,y) :- Mother(x,z), Ancestor(z,y).
 ?- Ancestor(x,y).
 /
+
+%%%%%%%%%%%%%%%%%%
+% Double recursion (not allowed)
+%%%%%%%%%%%%%%%%%%
+
+Male_ancestor(x,y) :- Father(x,y).
+Male_ancestor(x,y) :- Male_ancestor(x,z), Male_ancestor(z,y).
+?- Male_ancestor(x,y).
+/
+