Commit 1c25b11a authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Commit merges on datalog subdirectory from Clovis' branch

parent e52570f5
......@@ -38,7 +38,7 @@ PREVIOUS_DIRS =
# Source files in the right order of dependance
ML = signature.ml string_map.ml int_map.ml int_set.ml program.ml pmcfg.ml pmcfg_to_datalog.ml oriented_pmcfg.ml lexicalizer.ml pmcfg_syn.ml program_printer.ml prefix_correct_program.ml adornment2.ml magic_set_rewritting2.ml kanazawa_transform.ml datalog_solver.ml
ML = datalog_signature.ml string_map.ml int_map.ml int_set.ml program.ml pmcfg.ml pmcfg_to_datalog.ml oriented_pmcfg.ml lexicalizer.ml pmcfg_syn.ml program_printer.ml prefix_correct_program.ml adornment2.ml magic_set_rewritting2.ml kanazawa_transform.ml datalog_solver.ml
EXE_SOURCES = test.ml
......
open Signature
open Datalog_signature
open Program
open Int_set
module Adornment =
struct
type adornment = Ad of Signature.predicate*((int*bool) list)
type adorned_predicate = AdP of Signature.predicate*(bool list)
type adornment = Ad of Datalog_signature.predicate*((int*bool) list)
type adorned_predicate = AdP of Datalog_signature.predicate*(bool list)
type adorned_clause = ACl of adornment*(adornment list)
exception No_order_found
......@@ -31,14 +31,14 @@ struct
in
comp_list l1 l2
else
(Signature.compare_predicate p1 p2)
(Datalog_signature.compare_predicate p1 p2)
end
module Adorned_predicate_set=Set.Make (Ordered_adorned_predicates)
type adorned_program = AProg of
Signature.signature*Adorned_predicate_set.t*(adorned_clause list)
Datalog_signature.signature*Adorned_predicate_set.t*(adorned_clause list)
type prog_context =
Prog_context of
......@@ -85,11 +85,11 @@ struct
function AdP (k,l) ->
let trans b= if b then "b" else "f" in
let suffix = String.concat "" (List.map (trans) l) in
String.concat "_" [(Signature.get_name k sign);suffix]
String.concat "_" [(Datalog_signature.get_name k sign);suffix]
let predicate_of_adornment sign =
function AdP(k,l) ->
let (arity,name) = Signature.get_predicate k sign in
let (arity,name) = Datalog_signature.get_predicate k sign in
let trans b= if b then "b" else "f" in
let suffix = String.concat "" (List.map (trans) l) in
(arity,name^"_"^suffix)
......@@ -640,9 +640,9 @@ let reset_prog_context prog_context =
Program.Pred(k,vars)
in
match sign with
Signature.S(_,eq,neq) ->
Datalog_signature.S(_,eq,neq) ->
Program.Prog
(Signature.S (ad_sign,eq,neq),
(Datalog_signature.S (ad_sign,eq,neq),
List.map
(function ACl(rhs,lhs) ->
Program.Cl(
......
module Signature =
module Datalog_signature =
struct
type predicate = int
type signature = S of ((int*string) list * (int option) * (int option))
......@@ -10,6 +10,8 @@ module Signature =
let empty = S ([],None,None)
let make_pred (i:int) = (i:predicate)
let get_predicate k =
function S (l,_,_) -> List.nth l k
......
open Signature
open Datalog_signature
open Int_map
open Program
module Datalog_solver =
struct
open Program
module Program1 = Program
type item = It of (int*int list)
type eval_rule = ER of (predicate* predicate * predicate list * int Int_map.t ) (* the first predicate is the conclusion, the second is the next that need to be identified, the list contains the predicates that need to be proved and the int_map is the substitution that has been computed so far.*)
type eval_rule = ER of (Program1.predicate* Program1.predicate * Program1.predicate list * int Int_map.t ) (* the first predicate is the conclusion, the second is the next that need to be identified, the list contains the predicates that need to be proved and the int_map is the substitution that has been computed so far.*)
type result = RER of eval_rule | RIt of item
exception Not_unifiable
let get_eval_rule (Cl(lhs,rhs)) =
let make_item i l = It(i,l)
let get_eval_rule (Program1.Cl(lhs,rhs)) =
(match rhs with
[] -> failwith "get_eval_rule: rule with an empty right hand side?"
| pred::rhs_tl -> ER (lhs, pred, rhs_tl, Int_map.empty)
)
let instanciate (Pred(k,args)) subst =
let instanciate (Program1.Pred(k,args)) subst =
It(k,
List.fold_right
(function arg ->
......@@ -35,7 +37,7 @@ struct
let rec eliminate_eq_neq predicates eq neq subst =
(match predicates with
Pred(k,[arg1;arg2])::predicates_tl ->
Program1.Pred(k,[arg1;arg2])::predicates_tl ->
if k=eq
then
(try
......@@ -112,7 +114,7 @@ struct
type agenda = Item_set.t (*set containing pairs (predicate identifier, arg instanciation)*)
type memory = M of (Signature.signature*chart*eval_rules*agenda*(item list)*int*int*int)
type memory = M of (Datalog_signature.signature*chart*eval_rules*agenda*(item list)*int*int*int)
exception No_more_step
......@@ -126,16 +128,16 @@ struct
let agenda = Item_set.add item agenda in
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let ev_rule_known (ER(_,Pred(k,_),_,_)as ev_rule) (M(_,_,ev_rules,_,_,_,_,_)) =
let ev_rule_known (ER(_,Program1.Pred(k,_),_,_)as ev_rule) (M(_,_,ev_rules,_,_,_,_,_)) =
ER_set.mem ev_rule (Array.get ev_rules k)
let add_ev_rule (ER(_,Pred(k,_),_,_)as ev_rule) (M(sign,chart,ev_rules,agenda,facts,step,eq,neq)) =
let add_ev_rule (ER(_,Program1.Pred(k,_),_,_)as ev_rule) (M(sign,chart,ev_rules,agenda,facts,step,eq,neq)) =
Array.set ev_rules k (ER_set.add ev_rule (Array.get ev_rules k));
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let rec extend_eval_rule
(ER(res,Pred(k,args_pred),predicates,subst))
(ER(res,Program1.Pred(k,args_pred),predicates,subst))
(It(l,args_item))
(M(_,_,_,_,_,_,eq,neq) as mem)
=
......@@ -166,8 +168,8 @@ struct
(try
add_mem (instanciate res subst) mem
with Not_found ->
(match res with Pred(k,_) -> failwith ("PB: pred "^(string_of_int k))))
| (subst,(Pred(k,_) as pred)::predicates) ->
(match res with Program1.Pred(k,_) -> failwith ("PB: pred "^(string_of_int k))))
| (subst,(Program1.Pred(k,_) as pred)::predicates) ->
let ev_rule = (ER(res,pred,predicates,subst)) in
if ev_rule_known ev_rule mem
then mem
......@@ -231,18 +233,18 @@ struct
let init_solver program facts =
match program with
Prog(sign,clauses) ->
let n = Signature.fresh sign in
Program1.Prog(sign,clauses) ->
let n = Datalog_signature.fresh sign in
let chart = Array.make n (Item_map.empty) in
let ev_rules = Array.make n (ER_set.empty) in
let agenda = Item_set.empty in
let step = -1 in
let (eq,sign) = Signature.add_eq_get_id sign in
let (neq,sign) = Signature.add_neq_get_id sign in
let (eq,sign) = Datalog_signature.add_eq_get_id sign in
let (neq,sign) = Datalog_signature.add_neq_get_id sign in
let _ =
List.fold_left
(function () ->
function Cl(pred,(Pred(k,args) as fst)::rem) ->
function Program1.Cl(pred,(Program1.Pred(k,args) as fst)::rem) ->
let ev_rule = ER(pred,fst,rem,Int_map.empty) in
Array.set ev_rules k (ER_set.add ev_rule (Array.get ev_rules k))
|_ -> failwith "init_solver: the program contains a clause with no rhs."
......@@ -253,13 +255,13 @@ struct
M(sign,chart,ev_rules,agenda,facts,step,eq,neq)
let init_solver2 program list magic =
let Prog(sign,_) = program in
let Program1.Prog(sign,_) = program in
let (_,facts) =
List.fold_left
(function (n,l) ->
function string ->
try
let (_,pred) = Signature.find_pred_of_name string sign in
let (_,pred) = Datalog_signature.find_pred_of_name string sign in
(n+1,It(pred,[n;n+1])::l)
with
Not_found ->
......@@ -273,13 +275,13 @@ struct
(It(magic,[0])::(List.rev facts))
let init_solver3 program init_state list magic =
let Prog(sign,_) = program in
let Program1.Prog(sign,_) = program in
let facts =
List.fold_left
(function l ->
function (string,(state1,state2)) ->
try
let (_,pred) = Signature.find_pred_of_name string sign in
let (_,pred) = Datalog_signature.find_pred_of_name string sign in
It(pred,[state1;state2])::l
with
Not_found ->
......@@ -311,7 +313,7 @@ struct
Array.set
res
step0
((Signature.get_name k sign,args)::(Array.get res step0))
((Datalog_signature.get_name k sign,args)::(Array.get res step0))
)
set
()
......
open Adornment2
open Program
open Signature
open Datalog_signature
open Prefix_correct_program
open Program_printer
open Magic_set_rewritting2
......@@ -50,10 +50,10 @@ module Kanazawa_transform =
with Invalid_argument _ -> false
let transform_program program name=
let Program.Prog(Signature.S(l,_,neq) as sign,_) = program in
let Program.Prog(Datalog_signature.S(l,_,neq) as sign,_) = program in
let n = List.length l in
let program = Prefix_correct_program.prefix_correct_transform exceptions program in
let (_,id) = Signature.find_pred_of_name name sign in
let (_,id) = Datalog_signature.find_pred_of_name name sign in
let goal = Adornment.AdP(id,[true;false]) in
let ad_program =
Adornment.adorn_program
......@@ -76,7 +76,7 @@ module Kanazawa_transform =
let program =
PMCFG.naive_program_of_pmcfg (Oriented_pmcfg.orient_grammar grammar)
in
let Program.Prog(Signature.S (l,_,neq),_) = program in
let Program.Prog(Datalog_signature.S (l,_,neq),_) = program in
let n = List.length l in
let program = Prefix_correct_program.prefix_correct_transform exceptions program in
let PMCFG.Grammar(_,_,init_id) = grammar in
......@@ -101,7 +101,7 @@ module Kanazawa_transform =
let program =
PMCFG.program_of_pmcfg (Oriented_pmcfg.orient_grammar grammar)
in
let Program.Prog(Signature.S (l,_,neq),_) = program in
let Program.Prog(Datalog_signature.S (l,_,neq),_) = program in
let n = List.length l in
let program = Prefix_correct_program.prefix_correct_transform exceptions program in
let PMCFG.Grammar(_,_,init_id) = grammar in
......@@ -126,7 +126,7 @@ module Kanazawa_transform =
let program =
PMCFG_to_datalog.get_program (Oriented_pmcfg.orient_grammar grammar)
in
let Program.Prog(Signature.S (l,_,neq),_) = program in
let Program.Prog(Datalog_signature.S (l,_,neq),_) = program in
let n = List.length l in
let program = Prefix_correct_program.prefix_correct_transform exceptions program in
let PMCFG.Grammar(_,_,init_id) = grammar in
......
open Adornment2
open Signature
open Datalog_signature
open Program
open Int_map
......@@ -11,7 +11,7 @@ struct
type prog_context =
Prog_context of
Signature.signature*
Datalog_signature.signature*
((int*int) Adorned_predicate_map.t) *
int *
(Program.clause list)* (*group_I*)
......@@ -20,7 +20,7 @@ struct
type clause_context =
Cl_context of
Signature.signature * (*signature that is enriched with magic and supplementary predicates*)
Datalog_signature.signature * (*signature that is enriched with magic and supplementary predicates*)
((int*int) Adorned_predicate_map.t) * (*maps adorned predicates to their normal and magic counter-parts; when the two numbers are equal, this means that the predicate is extensional*)
string * (*prefix of the names of the new supplementary predicates*)
int * (* number 'i' of the current supplementary predicate *)
......@@ -39,7 +39,7 @@ struct
let sup_name k = "sup_"^(string_of_int k)^"_"
let mark_intensionality ad_program =
let Adornment.AProg(Signature.S (l,_,_),_,clauses) = ad_program in
let Adornment.AProg(Datalog_signature.S (l,_,_),_,clauses) = ad_program in
let n = (List.length l) - 1 in
let rec intensional res n =
if n=(-1)
......@@ -137,7 +137,7 @@ struct
)
in
let Adornment.AProg(sign,interesting_adornments,ad_clauses) = ad_program in
let Signature.S(_,eq,neq) = sign in
let Datalog_signature.S(_,eq,neq) = sign in
let ad_list = Adornment.Adorned_predicate_set.elements interesting_adornments in
let (_,l,map,_,new_eq,new_neq) =
List.fold_left
......@@ -161,7 +161,7 @@ struct
extensional_map,eq_opt,neq_opt)
with
Not_found ->
let (arity,name) = Signature.get_predicate pred sign in
let (arity,name) = Datalog_signature.get_predicate pred sign in
let new_eq = if(Some(pred)=eq) then Some(n) else eq_opt in
let new_neq = if(Some(pred)=neq) then Some(n) else neq_opt in
(n+1,
......@@ -173,7 +173,7 @@ struct
(0,[],Adorned_predicate_map.empty,Int_map.empty,None,None)
ad_list
in
(Signature.S(List.rev l,new_eq,new_neq), map)
(Datalog_signature.S(List.rev l,new_eq,new_neq), map)
let init_prog_context ad_program =
let (sign,map) = get_new_signature ad_program in
......@@ -249,7 +249,7 @@ struct
if remaining_lhs=[]
then (initial_rhs,sign)
else
let (sup_p,sign) = Signature.add_pred_get_id arity name sign in
let (sup_p,sign) = Datalog_signature.add_pred_get_id arity name sign in
let new_sup_pred = Program.Pred(sup_p,sup_vars) in
(new_sup_pred,sign)
in
......
open Pmcfg
open Signature
open Datalog_signature
open String_map
open Int_map
open Program
......@@ -36,13 +36,13 @@ module Oriented_pmcfg =
type 'a transformation_info =
{map_ord_cat_to_id: 'a Ordered_cat_map.t ;
ordered_cat_to_treat:Ordered_cat_set.t ;
old_sign : Signature.signature;
new_sign : Signature.signature}
old_sign : Datalog_signature.signature;
new_sign : Datalog_signature.signature}
let get_category ord_cat sign=
(match ord_cat with
Ord_cat(k,Arg_order arg_ord) ->
let (rank,name) = Signature.get_predicate k sign in
let (rank,name) = Datalog_signature.get_predicate k sign in
let arity = List.length arg_ord in
let is_order_id arg_ord=
let rec check_order_id l n =
......@@ -81,7 +81,7 @@ module Oriented_pmcfg =
let get_initial_trans_info ord_cat sign =
let (rank,name) = get_category ord_cat sign in
let new_sign = Signature.add_pred rank name Signature.empty in
let new_sign = Datalog_signature.add_pred rank name Datalog_signature.empty in
{map_ord_cat_to_id = Ordered_cat_map.add ord_cat 0 Ordered_cat_map.empty;
ordered_cat_to_treat = Ordered_cat_set.singleton ord_cat ;
old_sign=sign;
......@@ -93,9 +93,9 @@ module Oriented_pmcfg =
let id = Ordered_cat_map.find ord_cat trans_info.map_ord_cat_to_id in
(id,trans_info)
with Not_found ->
let id = Signature.fresh trans_info.new_sign in
let id = Datalog_signature.fresh trans_info.new_sign in
let (rank,name) = get_category ord_cat trans_info.old_sign in
let new_sign = Signature.add_pred rank name trans_info.new_sign in
let new_sign = Datalog_signature.add_pred rank name trans_info.new_sign in
let map = Ordered_cat_map.add ord_cat id trans_info.map_ord_cat_to_id in
let to_treat = Ordered_cat_set.add ord_cat trans_info.ordered_cat_to_treat in
(id,
......
open Signature
open Datalog_signature
open String_map
open Int_map
open Program
......@@ -10,7 +10,7 @@ struct
type rhs_cat = Rhs_cat of int*(int list)
type lhs_cat = Lhs_cat of int*((argument list) list)
type grule = R of lhs_cat*(rhs_cat list)
type grammar = Grammar of (Signature.signature*(grule list)*int)
type grammar = Grammar of (Datalog_signature.signature*(grule list)*int)
let is_rule_defining_cat cat grule =
match grule with
......@@ -27,8 +27,8 @@ struct
Grammar (sign,rules,init) ->
let new_sign =
(match sign with
Signature.S(l,_,_) ->
Signature.S(
Datalog_signature.S(l,_,_) ->
Datalog_signature.S(
List.map
(function (rank,name) ->(2*rank,name))
l
......@@ -39,9 +39,9 @@ struct
)
)
in
let (rg_eq,new_sign) = Signature.add_pred_get_id 4 "eq" new_sign in
let (eq,new_sign) = Signature.add_eq_get_id new_sign in
let (neq,new_sign) = Signature.add_neq_get_id new_sign in
let (rg_eq,new_sign) = Datalog_signature.add_pred_get_id 4 "eq" new_sign in
let (eq,new_sign) = Datalog_signature.add_eq_get_id new_sign in
let (neq,new_sign) = Datalog_signature.add_neq_get_id new_sign in
let string_predicates = String_map.empty in
let rec get_ranges_and_ext_pred_of_arg j l ranges ext_pred string_predicates sign=
(match l with
......@@ -68,9 +68,9 @@ struct
let a_pred = Program.Pred (id,[j;j+1]) in
get_ranges_and_ext_pred_of_arg (j+1) tl ranges (a_pred::ext_pred) string_predicates sign
with Not_found ->
let id = Signature.fresh sign in
let id = Datalog_signature.fresh sign in
let string_predicates = String_map.add a id string_predicates in
let sign = Signature.add_pred 2 a sign in
let sign = Datalog_signature.add_pred 2 a sign in
let a_pred = Program.Pred (id,[j;j+1]) in
get_ranges_and_ext_pred_of_arg (j+1) tl ranges (a_pred::ext_pred) string_predicates sign
)
......
open Signature
open Datalog_signature
open String_map
open Pmcfg
......@@ -24,7 +24,7 @@ open Lexicalizer.Lexicalizer
type parse_context =
Parse of
Signature.signature * (*signature under construction*)
Datalog_signature.signature * (*signature under construction*)
int * (*identifier of the start predicate*)
pos * (*position in the stream*)
((int* bool) String_map.t) * (*variables of a rule, it associates to the name of the variable its identifier (an int), a boolean which sepcifies whether the variable has an occurrence that has been processed in the right hand side of the current rule*)
......@@ -40,7 +40,7 @@ open Lexicalizer.Lexicalizer
let empty_parse_context =
Parse (Signature.empty,0,first_pos,String_map.empty,None,[],"",[],[],[],0,0,[])
Parse (Datalog_signature.empty,0,first_pos,String_map.empty,None,[],"",[],[],[],0,0,[])
let parse_error pos message =
let P(line,col) = pos in
......@@ -72,13 +72,13 @@ open Lexicalizer.Lexicalizer
let Parse(sign,start,pos,variables,lhs,rhs,pred,top_lhs_arg,lhs_arg,rhs_arg,arity,fresh,rules) =
parse_context in
(try
let (ar0,id) = Signature.find_pred_of_name name sign in
let (ar0,id) = Datalog_signature.find_pred_of_name name sign in
if ar = ar0
then (parse_context,id)
else parse_error pos
("The predicate "^name^" should have arity "^string_of_int (ar0)^" but is used with arity "^string_of_int(ar)^".")
with Not_found ->
let (id,sign) = Signature.add_pred_get_id ar name sign in
let (id,sign) = Datalog_signature.add_pred_get_id ar name sign in
let parse_context =
Parse(sign,start,pos,variables,lhs,rhs,pred,top_lhs_arg,lhs_arg,rhs_arg,arity,fresh,rules)
in
......
open Pmcfg
open Signature
open Datalog_signature
open String_map
open Int_map
open Program
......@@ -17,13 +17,13 @@ struct
module Pair_map = Map.Make(Ordered_int_pair)
let gen_eq_name pred k sign =
"eq_"^(Signature.get_name pred sign)^"_"^(string_of_int k)
"eq_"^(Datalog_signature.get_name pred sign)^"_"^(string_of_int k)
let get_program (Grammar(sign, rules, init) as grammar) =
let new_sign =
(match sign with
Signature.S(l,_,_) ->
Signature.S(
Datalog_signature.S(l,_,_) ->
Datalog_signature.S(
List.map
(function (rank,name) ->(2*rank,name))
l
......@@ -34,7 +34,7 @@ struct
)
)
in
let (eq,new_sign) = Signature.add_eq_get_id new_sign in
let (eq,new_sign) = Datalog_signature.add_eq_get_id new_sign in
let string_predicates = String_map.empty in
let rec get_ranges_and_ext_pred_of_arg j l ranges ext_pred string_predicates sign=
(match l with
......@@ -61,8 +61,8 @@ struct
with Not_found ->
let (id,sign) =
if a=""
then (Signature.add_eq_get_id sign)
else (Signature.add_pred_get_id 2 a sign)
then (Datalog_signature.add_eq_get_id sign)
else (Datalog_signature.add_pred_get_id 2 a sign)
in
let string_predicates = String_map.add a id string_predicates in
let a_pred = Program.Pred (id,[j;j+1]) in
......@@ -109,7 +109,7 @@ struct
(Pair_map.find (pred,kth) eq_predicates, sign, eq_predicates)
with Not_found ->
let name = (gen_eq_name pred kth sign) in
let (id,sign) = Signature.add_pred_get_id 4 name sign in
let (id,sign) = Datalog_signature.add_pred_get_id 4 name sign in
(id,sign,Pair_map.add (pred,kth) id eq_predicates)
)
in
......@@ -167,7 +167,7 @@ struct
(Pair_map.find (pred,arg_nb) eq_predicates,sign,eq_predicates,eq_pred_to_create)
with Not_found ->
let name = (gen_eq_name pred kth sign) in
let (id,sign) = Signature.add_pred_get_id 4 name sign in
let (id,sign) = Datalog_signature.add_pred_get_id 4 name sign in
(id,sign,Pair_map.add (pred,kth) id eq_predicates,((pred,kth),id)::eq_pred_to_create)
in
let eq_rhs = eq_rhs@[Program.Pred(id,[j;j+1;l;l+1])] in
......
open Signature
open Datalog_signature
open Int_map
open Program
open Int_set
......@@ -8,7 +8,7 @@ struct
type prog_context =
Prog_context of
Signature.signature *
Datalog_signature.signature *
((int list) Int_map.t) *
(Program.clause list)
......@@ -21,14 +21,14 @@ struct
type snd_pass_prog_context =
Prog_context_snd_pass of
Signature.signature *
Datalog_signature.signature *
((int list) Int_map.t) *
(Program.clause list) *
int
type clause_context_snd_pass =
Cl_snd_pass of
Signature.signature* (*the signature we currently work in*)
Datalog_signature.signature* (*the signature we currently work in*)
((int list) Int_map.t)* (*added_predicates*)
(Program.clause list) * (*clauses collected so far*)
int * (*nb of treated clauses*)
......@@ -46,14 +46,14 @@ struct
if n=rank
then (sign,l)
else
let id = Signature.fresh sign in
let id = Datalog_signature.fresh sign in
let sign =
Signature.add_pred n (name^"_"^(string_of_int (n/2))) sign
Datalog_signature.add_pred n (name^"_"^(string_of_int (n/2))) sign
in
add_pred rank name (n+2) sign (id::l)
in
(match sign with
Signature.S (decl,_,_)->
Datalog_signature.S (decl,_,_)->
let (_,new_sign,added_predicates)=
List.fold_left
(function (n,sign,added_predicates) ->
......@@ -308,7 +308,7 @@ struct
remaining_lhs
in
let (id,signature) =
Signature.add_pred_get_id
Datalog_signature.add_pred_get_id
(List.length vars)
("aux_"^(string_of_int n)^"_"^(string_of_int (List.length remaining_preds)))
signature
......
open Signature
open Datalog_signature
open Int_set
module Program =
struct
type predicate = Pred of (Signature.predicate*(int list))
module Signature1 = Datalog_signature
type predicate = Pred of (Signature1.predicate*(int list))
(*
a predicate is constituted with:
the identifier it has in the signature
......@@ -15,14 +18,20 @@ module Program =
a predicate (its left hand side)
a list of predicates (its right had side)
*)
type program = Prog of (Signature.signature*clause list)
type program = Prog of (Signature1.signature*clause list)
(*
a program is constituted with:
the signature in which predicates are declared
the list of its clauses
*)
let empty = Prog (Signature.empty, [])
let empty = Prog (Signature1.empty, [])
let make_pred p l = Pred(p,l)
let make_clause p l = Cl(p,l)