% Supported types: % integer (int), float (float), atom (id), string (string) % The types are the same as the corresponding Prolog types. % start_rule(RuleNumber) % Stores the numbers of rules % with which bottom-up evaluation can be started. % :- dynamic start_rule/1. % cursor(Pred, RuleNumber, BodyLiteralNumber, BindingPattern, Types) % Stores information about required cursors. % Pred: The predicate for the cursor. % RuleNumber: Rule number of the rule for the cursor. % BodyLiteralNumber: Body literal number within the rule of the literal % for which the cursor is created. % BindingPattern: a list consisting of b and f, representing a binding % pattern for calling the cursor. % Types: Types of the columns of the cursor. % %%%%%% IMPROVEMENT %%%%%% % TODO: If the cursor literal contains constants, these can be hard-coded into % the cursor and need not be transferred via a call. % :- dynamic cursor/5. % idb_pred_types(Predicate, Types) % Stores type information for idb predicates. % Predicate: the idb predicate name. % Types: a list of types for the predicate arguments. % :- dynamic idb_pred_types/2. % variable(RuleNumber, VariableNumber, Type) % Stores information about variables. % RuleNumber: The rule number for the variable. % VariableNumber: a number/identifier that identifies the variable within the % rule. % Type: The type of the variable. % :- dynamic variable/3. % application_edge(input_fact([InputFact], [ModifiedInputFact], InputEquations, InputAssignments), % EdgeNumber, % app_rule(RuleNumber, LitNumber, Line), NewRuleHead, CursorCalls, % Equations, Assignments) % % Stores an edge of the rule application graph with information for code % generation. % InputFact: Input fact for the rule as it is generated by rule application. % EdgeNumber: An identifying number for this edge. Helps to later associate % jump labels to edges. % It is stored as a list so that the empty list can be used for "no input". % ModifiedInputFact: In certain cases, e.g. when there are variable conflicts, % the input fact needs to be modified before it can be used with a rule. % This argument stores the modified fact. % InputEquations: This is a list of equal/2 facts that store information about % conditions that have to hold for runtime unification % InputAssignments: A list of assign/2 facts that store the % information how the modified fact can be obtained from the input fact. % RuleNumber: The number of the rule with which the input fact is used. % LitNumber: The number of the body literal that unifies with the input fact. % Line: The line of the source program where the code for this rule started; % for error messages. % NewRuleHead: The head of the rule after it has been used with the input fact % and the cursors % CursorCalls: A list of facts % cursor_call(Pred, RuleNumber, BodyLitNumber, BindingPattern, CallArgs) where % RuleNumber is the same as before, BodyLitNumber is the number of the % body literal for the cursor, BindingPattern is a list of b and f describing % the binding pattern of the cursor; and CallArgs is a list of atomics % or facts v(No, Id, Type) that describe the arguments for calling the cursor. % Equations: A list of facts equal/2 that describe conditions on the cursor % arguments; cursor arguments have the form c(RuleNumber, LitNo, ArgNo, BindingPattern, Type) where % RuleNumber is the same as before, LitNo is the literal number of the cursor % literal, ArgNo is the argument number of the literal/the cursor column, % and Type is the type of the argument/cursor column. % Assignments: Similar in form to Equations, only with facts % assign/2. Stores information about assignments to the variables that are used % in the rule head, which have the form v(No, Id, Type). % :- dynamic application_edge/7. % Identifying numbers for application edge facts. Used as counter. :- dynamic application_edge_number/1. % Stores the number of an application edge that leads to recursion. :- dynamic recursive/1. % Stores the name of a recursive predicate. :- dynamic recursive_pred/1. % Arg1: Prediate name % Arg2: List of argument types :- dynamic derivable_pred/2. :- dynamic rule_application_db/2. :- dynamic recursion_history_id/1. :- dynamic recursion_history_entry/2. :- dynamic recursion_history_edge/2. %------------------------------------------------------------------------------- % define_undefined % % Define every undefined body predicate as edb predicate with id argument % types %------------------------------------------------------------------------------- define_undefined :- findall(undefined(Pred, Arity), body_pred(Pred,Arity),Undefined), to_edb(Undefined). to_edb([]). to_edb([undefined(Pred,Arity)|Undefined]) :- length(List, Arity), fill_type_list(List, id), save_edb(Pred, List), to_edb(Undefined). fill_type_list([],_). fill_type_list([Type|Rest], Type) :- fill_type_list(Rest, Type). %------------------------------------------------------------------------------- % rule_variants % % For every rule, store variants so that every idb body literal is in a first % position (for efficient access). % If there is no idb body literal, the first position becomes the empty list. %------------------------------------------------------------------------------- rule_variants :- findall((First,No, FirstNo, Body,Head,Line),transformed_rule(First,No, FirstNo, Body, Head,Line), RuleList), make_variants(RuleList). % if the first body predicate is edb, check if the other predicates are also % edb. Then, this is a starting rule. Remove this rule, and replace it with % a rule where First is empty, but Body contains all body literals. make_variants([]). make_variants([(First,No,FirstNo, Body,Head, Line)|RuleList]) :- %if (First=[] -> true; First = [Elem], functor(Elem,Pred,_), %if (edb_pred(Pred,_) -> retract(transformed_rule(First,No, FirstNo, Body,Head, Line)), %if (check_edb_body(Body) -> assertz(transformed_rule([],No, 0, Body,Head, Line)) ; make_idb_variants(transformed_rule(First,No, FirstNo, Body,Head, Line)) ) ; %else : idb_pred(Pred,_) make_idb_variants(transformed_rule(First,No, FirstNo, Body, Head,Line)) ) ),!, make_variants(RuleList). check_edb_body([]). check_edb_body([First|Body]) :- functor(First,Func,_), edb_pred(Func,_), check_edb_body(Body). % is always called with first argument not the empty list! make_idb_variants(transformed_rule([First],No, _FirstNo, [First|Body], Head,Line)) :- findall(transformed_rule([Elem], No, ElemNo2, [First|Body], Head,Line),(nth1(ElemNo, Body,Elem), functor(Elem,Func,_),idb_pred(Func,_), ElemNo2 is ElemNo+1),VariantList), store_rule_variants(VariantList). store_rule_variants([]). store_rule_variants([Rule|VariantList]) :- % at this point it is checked whether we have generated % an already existing rule, but this case should be very rare copy_term(Rule, Rule2), call(Rule2), Rule =@= Rule2, !, store_rule_variants(VariantList). store_rule_variants([Rule|VariantList]) :- assertz(Rule), store_rule_variants(VariantList). %------------------------------------------------------------------------------- % abstract_bu_eval % % Abstract bottom-up evaluation. % Generates data for code generation. %------------------------------------------------------------------------------- abstract_bu_eval :- retractall(start_rule(_)), retractall(cursor(_,_,_,_,_)), retractall(idb_pred_types(_,_)), retractall(variable(_,_,_)), retractall(application_edge(_,_,_,_,_,_,_)), retractall(application_edge_number(_)), retractall(recursive(_)), retractall(recursive_pred(_)), retractall(derivable_pred(_,_)), retractall(rule_application_db(_,_)), retractall(recursion_history_id(_)), retractall(recursion_history_entry(_,_)), retractall(recursion_history_edge(_,_)), %retractall(rule_application_counter(_)), assertz(application_edge_number(1)), assertz(recursion_history_id(0)), %assertz(rule_application_counter(0)), collect_start_rules(StartRules), compute_app_start_rules(StartRules, AppStartRules), add_rule_applications(0, AppStartRules, Counter), rule_application_step(Counter) . collect_start_rules(StartRules) :- findall(r([], No, 0, Body,Head,Line),transformed_rule([], No, 0, Body,Head,Line), StartRules). compute_app_start_rules([], []). compute_app_start_rules([r([], No, 0, Body,Head,Line)|Rules], [app_rule(input_fact([],[],[], _InAssignments), 0, [], No, 0, Body, Head, Line)|AppRules]) :- compute_app_start_rules(Rules, AppRules). rule_application_step(0). rule_application_step(Counter) :- %[app_rule(InputFact, RecursionHistory, First, No, FirstNo, Body,Head,Line)|RuleList] integer(Counter), Counter>0, (Counter<50000 -> true; write('Error: too many rule application steps'),nl ), !, rule_application_db(Counter, app_rule(InputFact, RecursionHistoryID, First, No, FirstNo, Body,Head,Line)), nonvar(No), % Just testing if something went wrong at unification, avoid generating endless lists !, apply_rule(app_rule(InputFact, RecursionHistoryID, First, No, FirstNo, Body,Head,Line), AppResultList), (nonvar(AppResultList), AppResultList = [OldHead, CursorCalls, Equations, NewHead, Assignments]-> store_results(app_rule(InputFact, First, No, FirstNo, Body,NewHead,Line), RecursionHistoryID, NewRecursionHistoryID, CursorCalls, Equations, Assignments), %OldHead: original rule head with unbound variables find_next_rules(OldHead, NewHead, NewRecursionHistoryID, NextRules) %buildNewRuleList(NextRules, RuleList, NewRuleList) %NewRuleList=RuleList ; AppResultList = [], NextRules = [] %NewRuleList=RuleList ), retractall(rule_application_db(Counter,_)), Counter2 is Counter -1, add_rule_applications(Counter2, NextRules, CounterNew), %(Counter2 == CounterNew -> % CounterNext is Counter2-1 % ; % CounterNext = CounterNew %), %write(NextRules),nl, rule_application_step(CounterNew). rule_application_step(Counter) :- Counter >= 500000, write('Too many rule applications.'),fail. apply_rule(app_rule(input_fact(_InFact, ModifiedInFact, _InEquations, InAssignments), _RecursionHistory, First, No, FirstNo, Body,Head,_Line), AppResultList) :- %bu_method(push),!, % apply input fact, which is a list of a literal (possibly empty) copy_term(Head, OldHead), First = ModifiedInFact, %%% HIER HERLEITBARE PRÄDIKATE SUCHEN UND ÜBERGEBEN %%% create_apply_cursors(No, First, FirstNo, Body, 1, CursorResultList), (nonvar(CursorResultList), CursorResultList = [CursorCalls, Equations] -> Head =.. [HeadPred|HeadArgs], replace_head_args(HeadArgs, HeadArgs, No, 1, NewHeadArgs, HeadTypes, ModifiedInFact, InAssignments, Assignments), !, store_new_idb(HeadPred, HeadTypes), store_head_vars(NewHeadArgs), store_inAssign_vars(InAssignments), NewHead =.. [HeadPred|NewHeadArgs], AppResultList =[OldHead, CursorCalls, Equations, NewHead, Assignments] ; (CursorResultList == [] -> AppResultList = [] ; writ('Error at a rule application step'), nl, fail ) ) . create_apply_cursors(_,_,_,[],_, [[], []]). create_apply_cursors(No, First, FirstNo, [Lit|Body], BodyLitCount, CursorResultListOut) :- %nl,write('entering '), write(create_apply_cursors(No, First, FirstNo, [Lit|Body], BodyLitCount, CursorResultList)),nl, %bu_method(push),!, % First always contains IDB literal, if not empty (((First =..[PredFirst|ArgsFirst],length(ArgsFirst,LFirst),length(TypesFirst,LFirst),edb_pred(PredFirst,TypesFirst));FirstNo \= BodyLitCount) -> (FirstNo \= BodyLitCount -> Lit =.. [Pred | Args], length(Args, N), length(Types,N), ((edb_pred(Pred,Types); idb_pred_types(Pred, Types); derivable_pred(Pred, Types)) -> %%% HIER TEST EINFÜGEN %%% %nl,write('call '), write(create_cursor_args(No,BodyLitCount, 1, Args, Types, BindingPattern, BindingPattern, CallArgs, Eq)),nl, create_cursor_args(No,BodyLitCount, 1, Args, Types, BindingPattern, BindingPattern, CallArgs, Eq), %write('after '), write(create_cursor_args(No,BodyLitCount, 1, Args, Types, BindingPattern, BindingPattern, CallArgs, Eq)),nl, %EquationsOut = [Eq|Equations], store_cursor(cursor(Pred, No, BodyLitCount, BindingPattern, Types)), BLC is BodyLitCount+1, create_apply_cursors(No, First, FirstNo, Body, BLC, CursorResultList), (nonvar(CursorResultList), CursorResultList = [CursorCalls, Equations] -> CursorCallsOut = [cursor_call(Pred, No, BodyLitCount, BindingPattern, CallArgs)|CursorCalls], append(Eq, Equations, EquationsOut), CursorResultListOut = [CursorCallsOut, EquationsOut] ; CursorResultListOut = [] ) ; %write('Hi'),nl, CursorResultListOut = [] ) ; BLC is BodyLitCount+1, create_apply_cursors(No, First, FirstNo, Body, BLC, CursorResultList), (nonvar(CursorResultList), CursorResultList = [CursorCalls, Equations] -> CursorCallsOut = CursorCalls, EquationsOut = Equations, CursorResultListOut = [CursorCallsOut, EquationsOut] ; CursorResultListOut = [] ) ) %write('returning '), write(create_apply_cursors(No, First, FirstNo, [Lit|Body], BodyLitCount, CursorResultList)),nl . %append(Eq, Equations, EquationsOut). create_cursor_args(_No,_BodyLitCount, _ArgCount, [], [], [], _, [], []). create_cursor_args(No,BodyLitCount, ArgCount, [Arg|Args], [Type|Types], BindingPattern, FinalBindingPattern, CallArgsOut, EquationsOut) :- %if (var(Arg) -> B = f, Arg = c(No, BodyLitCount, ArgCount, FinalBindingPattern, Type), EquationsOut = Equations, CallArgsOut = CallArgs ; %if (Arg = v(_,_,VType) -> %if (Type = VType -> B = b, EquationsOut = Equations, CallArgsOut= [Arg|CallArgs] ; write('Error: Rule '), write(No), write('Body Literal '), write(BodyLitCount), write(' Argument '), write(ArgCount), write(': Type mismatch: Found '), write(VType), write(', required '), write(Type),nl, fail ) ; %if (Arg = c(_,_,_,_, CType) -> %if (CType = Type -> B = b, %this could also be f (Arg = c(No, BodyLitCount, _, _, _) -> EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount, FinalBindingPattern, Type))|Equations], CallArgsOut = CallArgs ; EquationsOut = Equations, CallArgsOut = [Arg|CallArgs] ) ; write('Error: Rule '), write(No), write('Body Literal '), write(BodyLitCount), write(' Argument '), write(ArgCount), write(': Type mismatch: Found '), write(CType), write(', required '), write(Type),nl, fail ) ; %if (atomic(Arg) -> B=b, CallArgsOut = [Arg|CallArgs], %if (integer(Arg), Type=int -> %EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations] EquationsOut = Equations ; (float(Arg), Type=float -> %EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations] EquationsOut = Equations ; %%% else %if (atom(Arg), Type=id -> %EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations] EquationsOut = Equations ; %if (string_codes(_,Arg),Type=string -> %EquationsOut = [equal(Arg,c(No, BodyLitCount,ArgCount,FinalBindingPattern, Type))|Equations] EquationsOut = Equations ; write('Error: Rule '), write(No), write('Body Literal '), write(BodyLitCount), write(' Argument '), write(ArgCount), write(': Type mismatch: Found '), write(Arg), write(', required '), write(Type),nl, fail ) ) ) ) ; write('Error: Rule '), write(No), write('Body Literal '), write(BodyLitCount), write(' Argument '), write(ArgCount), write(': No matching possible: '), write(Arg),nl, fail ) ) ) ), ArgCount2 is ArgCount+1, BindingPattern = [B|BP], create_cursor_args(No,BodyLitCount, ArgCount2, Args, Types, BP, FinalBindingPattern, CallArgs, Equations) . replace_head_args([],_,_,_,[], [],_, [],[]). replace_head_args([Arg|HeadArgs], AllHeadArgs, No, ArgCounter, [NewArg|NewHeadArgs], [Type|HeadTypes], ModifiedInFact,InAssignmentsOut, EquationsOut) :- bu_method(push),!, transformed_rule(_,No,_,_,Head,_), functor(Head,Pred,_), %if (Arg = c(No,_LitNo,_LitArgNo, _BindingPattern, Type) -> (bu_method(old_push) -> NewArg = v(Pred,ArgCounter,Type) ; NewArg = v(No,ArgCounter,Type) ), InAssignmentsOut = InAssignments, %EquationsOut = [assign(NewArg,Arg)|Equations] append(Equations, [assign(NewArg,Arg)], EquationsOut) ; %if (Arg = v(ArgOne,Count,Type) -> %%% im else-Teil die Variable No irgendwie durch ArgOne ersetzen bzw. Fehlermeldungen verbessern (\+bu_method(old_push),ArgOne==No,ModifiedInFact = [ModFact], ModFact =.. [_ModPred|ModArgs], member(Arg,ModArgs),integer(Count),nth1(Count,AllHeadArgs,c(No,_,_,_,_)) -> atomic_concat(old,Count,Count2), NewArg =.. [v,No,Count2,Type], InAssignmentsOut = [assign(NewArg,Arg)|InAssignments], EquationsOut = Equations ; (bu_method(old_push) -> (ArgOne==Pred -> (Count==ArgCounter -> NewArg = Arg, EquationsOut = Equations, InAssignmentsOut = InAssignments ; %atomic_concat(old,Count,Count2), %IntermediateArg =.. [v,Pred,Count2,Type], %InAssignmentsOut = [assign(IntermediateArg,Arg)|InAssignments], InAssignmentsOut = InAssignments, NewArg = v(Pred,ArgCounter,Type), %EquationsOut = [assign(NewArg,IntermediateArg)|Equations] EquationsOut = [assign(NewArg,Arg)|Equations] ) ; NewArg = v(Pred,ArgCounter,Type), EquationsOut = [assign(NewArg,Arg)|Equations], InAssignmentsOut = InAssignments ) ; NewArg = Arg, EquationsOut = Equations, InAssignmentsOut = InAssignments ) ) ; %if (atomic(Arg) -> NewArg=Arg, EquationsOut = Equations, InAssignmentsOut = InAssignments, %if (integer(Arg) -> Type = int ; (float(Arg) -> Type = float ; (atom(Arg) -> Type = id ; (string_codes(Arg,_) -> Type = string; write('Error: Cannot match type for argument '), write(ArgCounter), write(' of head of rule.'), %write(No), nl,fail ) ) ) ) ; write('Error: Invalid argument for head of rule.'), %write(No), nl, fail ) ) ), ArgCounter2 is ArgCounter+1, replace_head_args(HeadArgs,AllHeadArgs,No,ArgCounter2,NewHeadArgs,HeadTypes,ModifiedInFact,InAssignments, Equations) . % transformed_rule([], No, 0, Body,Head,Line) % app_rule(InputFact, First, No, FirstNo, Body,Head,Line) %find_next_rules(NextFirst, NewHead, RecursionHistoryID, NextRulesOut) :- % % findall(r(NewHead, NextFirst, NewNo, NewFirstNo, NewBody, NextHead, RecursionHistoryID, NewLine), transformed_rule([NextFirst], NewNo, NewFirstNo, NewBody, NextHead, NewLine) , NextRules), % %write('NextRules '),write(NextRules),nl, % remove_existing_next_rules(NextRules, NextRulesOut) % %write('NextRulesOut '),write(NextRulesOut),nl % . %find_next_rules(_OldHead, NewHead, RecursionHistoryID, NextRulesOut) :- find_next_rules(OldHead, NewHead, RecursionHistoryID, NextRulesOut) :- findall(r(NewHead, NextFirst, NewNo, NewFirstNo, NewBody, NextHead, RecursionHistoryID, NewLine), (transformed_rule([NextFirst], NewNo, NewFirstNo, NewBody, NextHead, NewLine), unifiable(NextFirst, OldHead,_)) , NextRules), %write('NextRules '),write(NextRules),nl, remove_existing_next_rules(NextRules, NextRulesOut), NewHead =.. [NewHeadPred|_], idb_pred_types(NewHeadPred, NewHeadTypes), NewHeadPred2 =.. [NewHeadPred|NewHeadTypes], (\+ derivable_pred(NewHeadPred, NewHeadTypes) -> assertz(derivable_pred(NewHeadPred, NewHeadTypes)) ; true ), find_derivable([NewHeadPred2], []) . buildNewRuleList(NextRules, RuleList, NewRuleList) :- bu_method(push),!, append(NextRules, RuleList, NewRuleList). %--------------------------------------------------------------- % remove_existing_next_rules/2 % % This predicate name is not good, the predicate does more than % only removing existing rule applications from the rule list %--------------------------------------------------------------- remove_existing_next_rules([],[]). % app_rule(InputFact, First, No, FirstNo, Body,Head,Line) % application_edge(InputFact, Nr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments) remove_existing_next_rules([r(NewHead, NextFirst, NewNo, NewFirstNo, NewBody, NextHead, RecursionHistoryID, NewLine)|NextRules], NextRulesOut) :- (application_edge(input_fact([NewHead],_, _Eq, _Ass),OldAppEdgeNr,app_rule(NewNo,NewFirstNo,NewLine),_,_,_,_) -> NextRulesOut = NR, (tag_recursive(OldAppEdgeNr, RecursionHistoryID) -> true ; true ) ; NewHead =.. [NextFirstPred|NewHeadArgs], NextFirst =.. [NextFirstPred|NextFirstArgs], NextHead =..[_|NextHeadArgs], copy_term((NextFirstArgs, NextHeadArgs), (ModifiedArgs, CopyNextHeadArgs)), ( apply_new_head(NewHeadArgs, NewNo, ModifiedArgs, Equations, Assignments, CopyNextHeadArgs) -> Modified =.. [NextFirstPred|ModifiedArgs], NextRulesOut = [app_rule(input_fact([NewHead], [Modified],Equations, Assignments), RecursionHistoryID, [NextFirst], NewNo, NewFirstNo, NewBody, NextHead, NewLine)|NR] ; %apply_new_head should always succeed (?) %NextRulesOut = NR fail ) ), remove_existing_next_rules(NextRules,NR). apply_new_head([],_,[], [], _,_). apply_new_head([NewArg|NewHeadArgs], NextNo, [ModArg|ModifiedArgs], Equations, Assignments, NextHeadArgs) :- % Fall Arg=String auch behandeln! \+atomic(Arg), string_codes(Arg,_),Type=string (var(ModArg) -> %(nonvar(NewArg),NewArg=v(NextNo,Count ,Type), mymember(ModArg,NextHeadArgs)-> % (integer(Count) -> % atomic_concat(old,Count,Count2), % ModArg = v(NextNo,Count2,Type), % % %Variable speichern % store_head_vars([v(NextNo,Count2,Type)]), % Assignments = [assign(v(NextNo,Count2,Type),NewArg)|Assignments2], % Equations = Equations2 % ; % write('Error: Danger of infinite variable creation:'),nl, % write('Rule '), write(NextNo), write('Variable '), write(v(NextNo,Count ,Type)), % nl, write('Trying to make it even older.'),!, % fail % ) % ; % ModArg=NewArg, % Equations = Equations2, % Assignments = Assignments2 ModArg=NewArg, Equations = Equations2, Assignments = Assignments2 ; (atomic(ModArg) -> (nonvar(NewArg),NewArg=v(_,_,Type) -> %Typen muessen uebereinstimmen! ((integer(ModArg), Type=int;float(ModArg),Type=float;atom(ModArg),Type=id) -> %Fall String auch behandeln!\+atomic(ModArg), string_codes(ModArg,_),Type=string Equations = [equal(NewArg,ModArg)|Equations2], Assignments = Assignments2 ; write('Error: Type mismatch in rule '), nl, transformed_rule(_, NextNo, _, RuleBody, RuleHead,_), write(RuleHead), write(' :- '), write(RuleBody),nl,fail ) % ; NewArg=ModArg, Equations = Equations2, Assignments = Assignments2 ) ; (nonvar(ModArg),ModArg = v(_,_,Type) -> ((NewArg=v(_,_,Type);integer(NewArg), Type=int;float(NewArg),Type=float;atom(NewArg),Type=id) -> Equations = [equal(NewArg,ModArg)|Equations2], Assignments = Assignments2 ; write('Error: Type mismatch in rule '), write(NextNo),nl,fail ) ; string_codes(ModArg,_) -> (nonvar(NewArg),NewArg=v(_,_,Type) -> Type=string, Equations = [equal(NewArg,ModArg)|Equations2], Assignments = Assignments2 ; NewArg=ModArg, Equations = Equations2, Assignments = Assignments2 ) ; write('Error in rule '), write(NextNo), nl, fail ) ) ),!, apply_new_head(NewHeadArgs, NextNo, ModifiedArgs, Equations2, Assignments2, NextHeadArgs). derivable_body([]). derivable_body([Lit|Body]) :- Lit =.. [Pred|Args], (edb_pred(Pred, Args); idb_pred_types(Pred, Args); derivable_pred(Pred, Args)), derivable_body(Body). derive_derivable_ruleList([], []). derive_derivable_ruleList([der_rule(NextHead, NextBody)|DerivedList], DerivedPreds) :- (derivable_body(NextBody) -> DerivedPreds = [NextHead|DerivedPreds2] ; DerivedPreds = DerivedPreds2 ), derive_derivable_ruleList(DerivedList, DerivedPreds2). find_derivable([], DerivedPreds) :- !, store_derivable(DerivedPreds, NewPreds), (NewPreds \= [] -> find_derivable(NewPreds, []) ; true ) . find_derivable([PredIn|PredList], DerivedPredsIn) :- copy_term(PredIn, Pred), %Pred =.. [PredName|_], %idb_pred_types(PredName, ArgTypes), %Pred2 =.. [PredName|ArgTypes], findall(der_rule(NextHead, NextBody), transformed_rule([Pred], _NextNo, _NextFirstNo, NextBody, NextHead, _NewLine), DerivedList), derive_derivable_ruleList(DerivedList, DerivedPreds), append(DerivedPredsIn, DerivedPreds, DerivedPreds2), find_derivable(PredList, DerivedPreds2). store_derivable([], []). store_derivable([Pred| PredList], NewPreds) :- Pred =.. [PredName|ArgTypes], (\+derivable_pred(PredName,_) -> assertz(derivable_pred(PredName, ArgTypes)), NewPreds = [Pred|NewPreds2] ; (derivable_pred(PredName,ArgTypes2), ArgTypes \= ArgTypes2 -> write('Error: Type clash for IDB predicate '), write(PredName), write(': '),nl, write('Types present: '), write(ArgTypes2), write(', Types to store: '), write(ArgTypes), nl, fail ; NewPreds = NewPreds2 ) ), store_derivable(PredList, NewPreds2). store_start_rules([]). store_start_rules([app_rule(_InputFact, [], No, 0, _Body,_Head,_Line)|Rules]) :- bu_method(push),!, assertz(start_rule(No)), store_start_rules(Rules) . store_cursor(cursor(Pred, No, BodyLitCount, BindingPattern, Types)) :- %if cursor(Pred, No, BodyLitCount, BindingPattern, Types2) -> %if (Types = Types2 -> true; write('Error in rule '), write(No), write(': Cursor '), write(cursor(Pred, No, BodyLitCount, BindingPattern)), write(' already exists with types '), write(Types2), nl, fail ) ; assertz(cursor(Pred, No, BodyLitCount, BindingPattern, Types)). store_new_idb(Pred, Types) :- idb_pred_types(Pred,Types), !. store_new_idb(Pred, Types) :- \+idb_pred_types(Pred,_) -> assertz(idb_pred_types(Pred,Types)) ; (idb_pred_types(Pred,Types) -> true ; write('Error: idb predicate '), write(Pred), write(' already exists with types '), write(Types), nl, fail ). store_head_vars([]). store_head_vars([Var|NewHeadArgs]) :- (Var=v(ArgOne,No,Type) -> ( variable(ArgOne,No,Type) -> true ; \+variable(ArgOne,No,_) -> assertz(variable(ArgOne,No,Type)) ; write('Error: variable '), write(variable(ArgOne,No,Type)), write(' already exists.'),nl, fail ) ; true ), store_head_vars(NewHeadArgs). store_inAssign_vars([]). store_inAssign_vars([assign(Var1, _)|InAssignments]) :- (Var1=v(ArgOne,No,Type) -> ( variable(ArgOne,No,Type) -> true ; \+variable(ArgOne,No,_) -> assertz(variable(ArgOne,No,Type)) ; write('Error: variable '), write(variable(ArgOne,No,Type)), write(' already exists.'),nl, fail ) ; write('Error: Left side of assignment is not a variable.'),nl ), store_inAssign_vars(InAssignments). %(member(No, RecursionHistory), \+ recursive(No) -> % assertz(recursive(No)) % ; % true %), %store_results(app_rule(InputFact, _First, No, FirstNo, _Body,NewHead,Line), RecursionHistory, [(AppEdgeNr,No)|RecursionHistory], CursorCalls, Equations, Assignments):- store_results(app_rule(InputFact, _First, No, FirstNo, _Body,NewHead,Line), RecHistID1, NewRecursionHistoryID, CursorCalls, Equations, Assignments):- (application_edge(InputFact,OldEdgeNr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments) -> %AppEdgeNr = OldEdgeNr recursion_history_id(RecursionHistoryID), NewRecursionHistoryID is RecursionHistoryID +1, retractall(recursion_history_id(_)), assertz(recursion_history_id(NewRecursionHistoryID)), assertz(recursion_history_entry(NewRecursionHistoryID,OldEdgeNr)) ; application_edge_number(AppEdgeNr), (AppEdgeNr >= 4000000 -> write('Too many application edges.'),fail ; assertz(application_edge(InputFact, AppEdgeNr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments)), retract(application_edge_number(AppEdgeNr)), AppEdgeNr2 is AppEdgeNr+1, assertz(application_edge_number(AppEdgeNr2)), (is_recursive(No, RecHistID1), \+recursive(AppEdgeNr) -> assertz(recursive(AppEdgeNr)), functor(NewHead,HeadPred,_), (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true) ; true ), recursion_history_id(RecursionHistoryID), NewRecursionHistoryID is RecursionHistoryID +1, retractall(recursion_history_id(_)), assertz(recursion_history_id(NewRecursionHistoryID)), assertz(recursion_history_entry(NewRecursionHistoryID,AppEdgeNr)) ) ), assertz(recursion_history_edge(NewRecursionHistoryID, RecHistID1)) . add_rule_applications(CounterIn, [], CounterIn). add_rule_applications(CounterOld, [Rule|RuleList], Counter2) :- add_rule_applications(CounterOld, RuleList, CounterNew), Counter2 is CounterNew + 1, assertz(rule_application_db(Counter2, Rule)). % application_edge(InputFact,EdgeNr, app_rule(No,FirstNo,Line), NewHead, CursorCalls, Equations, Assignments) is_recursive(RuleNr, RecHistID) :- recursion_history_entry(RecHistID,AppEdgeNr), application_edge(_,AppEdgeNr,app_rule(RuleNr,_,_),_,_,_,_), !. is_recursive(RuleNr, RecHistID) :- recursion_history_entry(RecHistID,AppEdgeNr), application_edge(_,AppEdgeNr,app_rule(RuleNr2,_,_),_,_,_,_), RuleNr \= RuleNr2, recursion_history_edge(RecHistID, RecHistID2), is_recursive(RuleNr, RecHistID2). %tag_recursive(AppEdgeNr, RecHistId) :- % recursion_history_entry(RecHistId,AppEdgeNr), % (\+ recursive(AppEdgeNr) -> % assertz(recursive(AppEdgeNr)), % application_edge(_InputFact, AppEdgeNr, app_rule(_No,_FirstNo,_Line), NewHead, _CursorCalls, _Equations, _Assignments), % functor(NewHead,HeadPred,_), % (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true) % ; % true % ), % !. %tag_recursive(AppEdgeNr, RecursionHistoryIDIn) :- % recursion_history_entry(RecursionHistoryIDIn,AppEdgeNr2), % AppEdgeNr \= AppEdgeNr2, % recursion_history_edge(RecursionHistoryIDIn, RecHistIDNext), % tag_recursive(AppEdgeNr, RecHistIDNext) % % . tag_recursive(AppEdgeNr, RecHistId) :- recursion_history_entry(RecHistId,AppEdgeNr), (\+ recursive(AppEdgeNr) -> assertz(recursive(AppEdgeNr)), application_edge(_InputFact, AppEdgeNr, app_rule(_No,_FirstNo,_Line), NewHead, _CursorCalls, _Equations, _Assignments), functor(NewHead,HeadPred,_), (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true) ; true ), !. tag_recursive(AppEdgeNr, RecursionHistoryIDIn) :- recursion_history_entry(RecursionHistoryIDIn,AppEdgeNr2), AppEdgeNr \= AppEdgeNr2, recursion_history_edge(RecursionHistoryIDIn, RecHistIDNext), tag_recursive(AppEdgeNr, RecHistIDNext), (\+ recursive(AppEdgeNr2) -> assertz(recursive(AppEdgeNr2)), application_edge(_InputFact, AppEdgeNr2, app_rule(_No,_FirstNo,_Line), NewHead, _CursorCalls, _Equations, _Assignments), functor(NewHead,HeadPred,_), (\+ recursive_pred(HeadPred) -> assertz(recursive_pred(HeadPred));true) ; true ) .