cacol89 avatar cacol89 committed 406e223 Merge

Merge branch 'feature/recursion' into develop

Comments (0)

Files changed (11)

     parser\
     lexer\
     yadi_utils\
+    rule_preproc\
     stratification\
     eval\
     conn_ops\
 DEP_expr=
 DEP_parser=expr
 DEP_lexer=parser
-DEP_eval=expr yadi_utils stratification
+DEP_eval=expr yadi_utils stratification rule_preproc
 DEP_conn_ops=expr yadi_utils
 DEP_yadi_utils=expr
 DEP_stratification=expr yadi_utils
 DEP_query_flattening=expr
+DEP_rule_preproc=expr yadi_utils
 
 #Rule for generating the final executable file
 bin/$(EX_NAME): $(FILES:%=bin/%.cmo) bin/$(MAIN_FILE).cmo
 bin/yadi_utils.cmo: $(DEP_yadi_utils:%=bin/%.cmo)
 bin/query_flattening.cmo: $(DEP_query_flattening:%=bin/%.cmo)
 bin/stratification.cmo: $(DEP_stratification:%=bin/%.cmo)
+bin/rule_preproc.cmo: $(DEP_rule_preproc:%=bin/%.cmo)
 
 clean:
 	rm -f bin/*.cmo bin/*.cmi src/parser.mli src/parser.ml src/lexer.ml 
 
 open Expr ;;
 open Yadi_utils;;
+open Rule_preproc;;
 open Stratification;;
 
 (** get the query expression, 
             | h::_ -> raise (Yadi_error "The program has more than one query")
 ;;
 
-(**Takes a program and extracts all rules and places them in
-* a symtable*)
-let extract_idb = function
-    | Prog stt_lst ->
-        let idb:symtable = Hashtbl.create 100 in
-        let in_stt t = match t with
-            | Rule _ -> symt_insert idb t 
-            | Query _ -> () in            
-        List.iter in_stt stt_lst;
-        idb
-
-(** Given a symtable, performs preprocess operations over the rules
- * contained in it. This operations are:
- *  - Extraction of constants in predicates
- *  - (TO BE IMPLEMENTED) Flattening of rules
- *)
-let preprocess_rules (st:symtable) =
-    let rep_rule key rules =
-        let rep_lst = List.map extract_rule_constants rules in
-        Hashtbl.replace st key rep_lst in
-    Hashtbl.iter rep_rule st
-
 (** Given a list of rterms, returns the SQL that must be in the from clause.
  * All the tables are aliased with the postfix '_aX_Y', where X is the arity of
  * the predicate and Y is the position of the goal in the rule, starting by 0.
                             (List.combine pred_names sql_lst) in 
     let strat_sql =
         if aug_sql_lst = [] then ""
-        else "WITH "^(String.concat ", " aug_sql_lst)
+        else "WITH RECURSIVE "^(String.concat ", " aug_sql_lst)
     in
     (** Calculate query's SQL*)
     let q_sql = sql_of_rule idb cnt qrule in
  * the database's edb description.
  * The boolean variable debug indicates whether debugging information
  * should be printed*)
-let sql_stt debug (edb:symtable) prog =
+let sql_stt (debug:bool) (edb:symtable) prog =
     let query_rt = get_query_rterm (get_query prog) in
     (*Extract and pre-process the IDB from the program*)
     let idb = extract_idb prog in
         List.fold_left extract_rterm [] t
     | Query _    -> invalid_arg "function get_all_rule_rterms called with a query"
 
-(** Extracts constants in a rterm and replaces them with
- * ad-hoc NumVars which numbers start from 'pos'. The function
- * returns a tuple with the new rterm and a list of equalities
- * that must be satisfied by the ad-hoc variables.
- *)
-let extract_rterm_constants ?(pos = 0) rt = match rt with
-    | Pred (x, vl) ->
-        let extract var (v_lst,e_lst,i) = match var with 
-            | ConstVar const -> 
-                let nvar = NumberedVar i in
-                let neq = Equal (nvar,const) in
-                (nvar::v_lst, neq::e_lst,i+1) 
-            | _ -> (var::v_lst, e_lst, i) in
-        let (vars,eqs,_) = List.fold_right extract vl ([],[],pos) in 
-        ( Pred (x,vars), eqs )
-
-(** Given a rule, extracts all constants in its head and body rterms
- * for replacing them with ad-hoc variables placed in the body.
- * E.g. "Q(a,b,1) :- P(1,a,c) and R(b,3)." will be transformed to
- * "Q(a,b,_0) :- P(_1,a,c) and R(b_2) and _0 = 1 and _1 = 1 and _2 = 3."
- *)
-let extract_rule_constants = function
-    | Query _    -> invalid_arg "function extract_rule_constants called with a query"
-    | Rule(h, b) -> 
-        let (h2, h2_e) = extract_rterm_constants h in
-        let extract t (t_lst,e_lst,i) = match t with
-            | Rel rt -> 
-                let (rt2,rt2_e) = extract_rterm_constants ~pos:i rt in
-                ((Rel rt2)::t_lst, rt2_e@e_lst, i+(List.length rt2_e) )
-            | _ -> (t::t_lst, e_lst, i) in
-        let (b2,b2_e,_) = List.fold_right extract b ([],[],(List.length h2_e)) in
-        Rule (h2,b2@h2_e@b2_e)
-;;
 
 (****************************************************
  *

src/rule_preproc.ml

+(*******************************************************)
+(**  rule_preproc.ml
+ *
+ *   Functions for preprocesing of IDB rules before
+ *   SQL generation.
+ *
+ *   @author cruelcoderz
+ * 
+ *)
+(********************************************************)
+
+open Expr;;
+open Yadi_utils;;
+
+(****************************************************)
+(*      Recursion check functions                   *)
+(****************************************************)
+
+(** Returns true if the provided term is a call to the predicate described
+ * by the provided key. If the recursive call is negative, an error is raised*)
+let rec check_rec_term key = function
+    | Rel rt ->
+        let rt_key = symtkey_of_rterm rt in
+        (key_comp key rt_key) = 0
+    | Not t ->
+        if (check_rec_term key t) then
+            raise (Yadi_error (
+                "Predicate "^(string_of_symtkey key)^
+                " is negatively recursive"
+            ))
+        else false
+    | _ -> false
+
+(** 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 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"
+            ))
+        | _ -> nr_lst@r_lst
+
+(****************************************************)
+(*      Constant extraction functions               *)
+(****************************************************)
+
+(** Extracts constants in a rterm and replaces them with
+ * ad-hoc NumVars which numbers start from 'pos'. The function
+ * returns a tuple with the new rterm and a list of equalities
+ * that must be satisfied by the ad-hoc variables.
+ *)
+let extract_rterm_constants ?(pos = 0) rt = match rt with
+    | Pred (x, vl) ->
+        let extract var (v_lst,e_lst,i) = match var with 
+            | ConstVar const -> 
+                let nvar = NumberedVar i in
+                let neq = Equal (nvar,const) in
+                (nvar::v_lst, neq::e_lst,i+1) 
+            | _ -> (var::v_lst, e_lst, i) in
+        let (vars,eqs,_) = List.fold_right extract vl ([],[],pos) in 
+        ( Pred (x,vars), eqs )
+
+(** Given a rule, extracts all constants in its head and body rterms
+ * for replacing them with ad-hoc variables placed in the body.
+ * E.g. "Q(a,b,1) :- P(1,a,c) and R(b,3)." will be transformed to
+ * "Q(a,b,_0) :- P(_1,a,c) and R(b_2) and _0 = 1 and _1 = 1 and _2 = 3."
+ *)
+let extract_rule_constants = function
+    | Query _    -> invalid_arg "function extract_rule_constants called with a query"
+    | Rule(h, b) -> 
+        let (h2, h2_e) = extract_rterm_constants h in
+        let extract t (t_lst,e_lst,i) = match t with
+            | Rel rt -> 
+                let (rt2,rt2_e) = extract_rterm_constants ~pos:i rt in
+                ((Rel rt2)::t_lst, rt2_e@e_lst, i+(List.length rt2_e) )
+            | _ -> (t::t_lst, e_lst, i) in
+        let (b2,b2_e,_) = List.fold_right extract b ([],[],(List.length h2_e)) in
+        Rule (h2,b2@h2_e@b2_e)
+;;
+
+(****************************************************)
+(*      Main function                               *)
+(****************************************************)
+
+(** 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, only one recursive call,
+ *      and not negated recursions)
+ *)
+let preprocess_rules (st:symtable) =
+    let rep_rule key rules =
+        let rep_lst = List.map extract_rule_constants rules in
+        let sorted_lst = check_rec_rule rep_lst in
+        Hashtbl.replace st key sorted_lst in
+    Hashtbl.iter rep_rule st

src/stratification.ml

     let sons = get_idb_graph_sons edb idb key in
     let rec_call son =
         if SymtkeySet.mem son (!visit) then
-            if SymtkeySet.mem son (!active) then
+            if (key_comp son key) != 0 && SymtkeySet.mem son (!active) then
                 raise (Yadi_error (
                     "Predicate "^(string_of_symtkey son)^
-                    " is recursive."
+                    " is indirectly recursive."
                 ))
             else []
         else
  * is returned as a list of IDB symtkeys, where the first key is the
  * first IDB relation to calculate in the stratification.
  * If the provided program contains references to undefined predicates,
- * the function will raise an exception.*)
+ * the function will raise an exception.
+ * *)
 let stratify (edb:symtable) (idb:symtable) (query_rt:rterm) : (symtkey list) =
     let visit = ref SymtkeySet.empty in
     let active = ref SymtkeySet.empty in

src/yadi_utils.ml

 let string_of_symtkey ((n,a):symtkey) =
     n^"/"^(string_of_int a)
 
+(**Takes a program and extracts all rules and places them in
+* a symtable*)
+let extract_idb = function
+    | Prog stt_lst ->
+        let idb:symtable = Hashtbl.create 100 in
+        let in_stt t = match t with
+            | Rule _ -> symt_insert idb t 
+            | Query _ -> () in            
+        List.iter in_stt stt_lst;
+        idb
+
 (***********************************************************
  *  kset (SymtkeySet)
  *********************************************************)

test/expected/integration/family.out

 | Homer  | Homer  |
 -------------------
 
+yadi$ 
+--------------------
+| col0    | col1   |
+--------------------
+| Homer   | Bart   |
+| Homer   | Lisa   |
+| Homer   | Maggie |
+| Abraham | Homer  |
+| Abraham | Herb   |
+| Clancy  | Marge  |
+| Clancy  | Patty  |
+| Clancy  | Selma  |
+| Abraham | Bart   |
+| Abraham | Maggie |
+| Abraham | Lisa   |
+--------------------
+
+yadi$ 
+--------------------
+| col0    | col1   |
+--------------------
+| Homer   | Bart   |
+| Homer   | Lisa   |
+| Homer   | Maggie |
+| Abraham | Homer  |
+| Abraham | Herb   |
+| Clancy  | Marge  |
+| Clancy  | Patty  |
+| Clancy  | Selma  |
+| Marge   | Bart   |
+| Marge   | Lisa   |
+| Marge   | Maggie |
+| Mona    | Homer  |
+| Mona    | Herb   |
+| Jackie  | Marge  |
+| Jackie  | Patty  |
+| Jackie  | Selma  |
+| Mona    | Bart   |
+| Mona    | Maggie |
+| Mona    | Lisa   |
+| Abraham | Bart   |
+| Abraham | Maggie |
+| Abraham | Lisa   |
+| Clancy  | Bart   |
+| Clancy  | Lisa   |
+| Clancy  | Maggie |
+| Jackie  | Bart   |
+| Jackie  | Lisa   |
+| Jackie  | Maggie |
+--------------------
+
 yadi$ 

test/expected/integration/family2.out

+
+yadi$ YADI execution error: Predicate Ancestor1/2 is indirectly recursive.
+
+yadi$ YADI execution error: Predicate P/1 is indirectly recursive.
+
+yadi$ YADI execution error: Predicate Q/1 is negatively recursive
+
+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$ 

test/integration/employees2.datalog

-%This file contains test cases with errors
+%............................................
+%............................................
+%............................................
+% All the test cases in this file contain
+% sintactic/semantic errors: they test if
+% yadi discovers and reports the errors.
+%............................................
+%............................................
+%............................................
 
 %%%%%%%%%%%%%%%%%
 % WRONG ARITY

test/integration/family.datalog

 /
 
 
-%Male_ancestor(x,y) :- Father(x,y).
-%Male_ancestor(x,y) :- Father(x,z), Male_ancestor(z,y).
-%?- Male_ancestor(x,y).
-%/
+%%%%%%%%%%%%%%%%%
+% Direct recursion
+%%%%%%%%%%%%%%%%%
+
+Male_ancestor(x,y) :- Father(x,y).
+Male_ancestor(x,y) :- Father(x,z), Male_ancestor(z,y).
+?- Male_ancestor(x,y).
+/
+
+Ancestor(x,y) :- Parent(x,z), Ancestor(z,y).
+Ancestor(x,y) :- Parent(x,y).
+Parent(x,y) :- Father(x,y).
+Parent(x,y) :- Mother(x,y).
+?- Ancestor(x,y).
+/
 

test/integration/family2.datalog

+%............................................
+%............................................
+%............................................
+% All the test cases in this file contain
+% sintactic/semantic errors: they test if
+% yadi discovers and reports the errors.
+%............................................
+%............................................
+%............................................
+
+%%%%%%%%%%%%%%%%%
+% Indirect recursion (not allowed)
+%%%%%%%%%%%%%%%%%
+
+Ancestor1(x,y) :- Father(x,y).
+Ancestor1(x,y) :- Father(x,z), Ancestor2(z,y).
+Ancestor2(x,y) :- Mother(x,y).
+Ancestor2(x,y) :- Mother(x,z), Ancestor1(z,y).
+Q(x,y) :- Ancestor1(x,y).
+Q(x,y) :- Ancestor2(x,y).
+?- Q(x,y).
+/
+
+P(x) :- Q(x).
+Q(x) :- R(x), not P(x).
+R(x) :- Mother(x,_).
+?- P(x).
+/
+
+%%%%%%%%%%%%%%%%%%
+%% Negative recursion (not allowed)
+%%%%%%%%%%%%%%%%%%
+
+Q(x) :- Father(x,_).
+Q(x) :- Mother(x,_), not Q(x).
+?- Q(x).
+/
+
+%%%%%%%%%%%%%%%%%%
+% Multiple recursion (not allowed)
+%%%%%%%%%%%%%%%%%%
+
+Ancestor(x,y) :- Father(x,y).
+Ancestor(x,y) :- Mother(x,y).
+Ancestor(x,y) :- Father(x,z), Ancestor(z,y).
+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).
+/
+
Tip: Filter by directory path e.g. /media app.js to search for public/media/app.js.
Tip: Use camelCasing e.g. ProjME to search for ProjectModifiedEvent.java.
Tip: Filter by extension type e.g. /repo .js to search for all .js files in the /repo directory.
Tip: Separate your search with spaces e.g. /ssh pom.xml to search for src/ssh/pom.xml.
Tip: Use ↑ and ↓ arrow keys to navigate and return to view the file.
Tip: You can also navigate files with Ctrl+j (next) and Ctrl+k (previous) and view the file with Ctrl+o.
Tip: You can also navigate files with Alt+j (next) and Alt+k (previous) and view the file with Alt+o.