Commit acf9bb90 authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Merge branch 'change_log'

Remove the dependency to BOLT and camlp4
parents 6a702d8b 63136f42
......@@ -23,6 +23,12 @@ lib: [
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__IdGenerator.cmti" {"utilsLib/utilsLib__IdGenerator.cmti"}
"_build/install/default/lib/acgtkLib/utilsLib/idGenerator.mli" {"utilsLib/idGenerator.mli"}
"_build/install/default/lib/acgtkLib/utilsLib/idGenerator.ml" {"utilsLib/idGenerator.ml"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__Log.cmi" {"utilsLib/utilsLib__Log.cmi"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__Log.cmx" {"utilsLib/utilsLib__Log.cmx"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__Log.cmt" {"utilsLib/utilsLib__Log.cmt"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__Log.cmti" {"utilsLib/utilsLib__Log.cmti"}
"_build/install/default/lib/acgtkLib/utilsLib/log.mli" {"utilsLib/log.mli"}
"_build/install/default/lib/acgtkLib/utilsLib/log.ml" {"utilsLib/log.ml"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__SharedForest.cmi" {"utilsLib/utilsLib__SharedForest.cmi"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__SharedForest.cmx" {"utilsLib/utilsLib__SharedForest.cmx"}
"_build/install/default/lib/acgtkLib/utilsLib/utilsLib__SharedForest.cmt" {"utilsLib/utilsLib__SharedForest.cmt"}
......
......@@ -9,9 +9,9 @@ build: [
depends: [
"dune" {build}
"dypgen"
"camlp4"
"bolt"
"ANSITerminal"
"fmt"
"logs"
"cairo2"
"yojson"
"easy-format"
......
......@@ -14,9 +14,9 @@ install: ["dune" "install"]
depends: [
"dune" {build}
"dypgen"
"camlp4"
"bolt"
"ANSITerminal"
"fmt"
"logs"
"cairo2"
"yojson"
"easy-format"
......
......@@ -21,9 +21,10 @@ open UtilsLib
open Logic
open Abstract_syntax
open Lambda
(*open DatalogLib *)
open Signature
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.acg_lexicon" ~doc:"logs ACGtkLib acg_lexicon events") : Logs.LOG)
module Make (Sg:Interface.Signature_sig with type term = Lambda.term and type stype = Lambda.stype) =
struct
......@@ -34,6 +35,9 @@ struct
module Dico = Utils.StringMap
module Signature=Sg
type signature = Sg.t
type resume = int SharedForest.SharedForest.resumption
......@@ -174,19 +178,23 @@ struct
(* interpreted_type *)
(if interpret_linear_arrow_as_non_linear lex then Lambda.unlinearize_type interpreted_type else interpreted_type)
lex.object_sig in
LOG "term: %s:%s" (Sg.term_to_string interpreted_term lex.object_sig) (Sg.type_to_string interpreted_type lex.object_sig) LEVEL TRACE;
LOG "eta-long form: %s" (Sg.term_to_string eta_long_term lex.object_sig) LEVEL TRACE;
LOG "eta-long form (as caml term): %s" (Lambda.raw_to_caml eta_long_term) LEVEL TRACE;
LOG "Datalog rule addition: lexicon \"%s\", constant \"%s:%s\" mapped to \"%s:%s\"" (fst lex.name) name (Sg.type_to_string abs_type lex.abstract_sig) (Sg.term_to_string eta_long_term lex.object_sig) (Sg.type_to_string interpreted_type lex.object_sig) LEVEL TRACE;
Log.info (fun m -> m "term: %s:%s" (Sg.term_to_string interpreted_term lex.object_sig) (Sg.type_to_string interpreted_type lex.object_sig));
Log.info (fun m -> m "eta-long form: %s" (Sg.term_to_string eta_long_term lex.object_sig));
Log.info (fun m -> m "eta-long form (as caml term): %s" (Lambda.raw_to_caml eta_long_term));
Log.info (fun m -> m "Datalog rule addition: lexicon \"%s\", constant \"%s:%s\" mapped to \"%s:%s\"" (fst lex.name) name (Sg.type_to_string abs_type lex.abstract_sig) (Sg.term_to_string eta_long_term lex.object_sig) (Sg.type_to_string interpreted_type lex.object_sig));
let obj_princ_type,obj_typing_env = TypeInference.Type.inference eta_long_term in
LOG "Interpreting \"%s\" as \"%s=%s\" with principle type: \"%s\"" name (Sg.term_to_string eta_long_term lex.object_sig) (Lambda.raw_to_caml eta_long_term) (Lambda.raw_type_to_string obj_princ_type) LEVEL DEBUG;
LOG "In the context of:" LEVEL DEBUG ;
(Utils.IntMap.iter
(fun k (t,ty) -> LOG "%d --> %s : %s" k (Lambda.raw_to_string t) (Lambda.raw_type_to_string ty) LEVEL DEBUG)
obj_typing_env);
let rule,new_prog=Reduction.generate_and_add_rule
~abs_cst:(name,abs_type)
~obj_princ_type
Log.info (fun m -> m "Interpreting \"%s\" as \"%s=%s\" with principle type: \"%s\"" name (Sg.term_to_string eta_long_term lex.object_sig) (Lambda.raw_to_caml eta_long_term) (Lambda.raw_type_to_string obj_princ_type));
Log.info (fun m -> m "In the context of:");
Log.info (fun m ->
let () =
(Utils.IntMap.iter
(fun k (t,ty) -> Log.debug (fun m -> m "%d --> %s : %s" k (Lambda.raw_to_string t) (Lambda.raw_type_to_string ty)))
obj_typing_env) in
m "Done.");
let rule,new_prog =
Reduction.generate_and_add_rule
~abs_cst:(name,abs_type)
~obj_princ_type
~obj_typing_env
prog
~abs_sig:lex.abstract_sig
......@@ -273,35 +281,30 @@ struct
let parse term dist_type lex =
match lex.datalog_prog,Sg.expand_type dist_type lex.abstract_sig with
| None,_ ->
let () = Printf.printf "Parsing is not implemented for non 2nd order ACG\n!" in
| None,_ ->
let () = Logs.warn (fun m -> m "Parsing is not implemented for non 2nd order ACG.") in
SharedForest.SharedForest.empty
(* | Some (prog,_), (Lambda.Atom _ as dist_type) -> *)
| Some {prog}, (Lambda.Atom _ as dist_type) ->
(* let pre_parse_time = Sys.time () in *)
LOG "Before parsing. Program is currently:" LEVEL DEBUG;
LOG "That's all.%s"
(let () =
let buff=Buffer.create 80 in
let () = Buffer.add_buffer buff (DatalogAbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract prog)) in
Utils.log_iteration
(fun s -> LOG s LEVEL DEBUG)
(Buffer.contents buff) in "") LEVEL DEBUG;
Log.info (fun m -> m "Before parsing. Program is currently:");
DatalogAbstractSyntax.Program.log_content Logs.Info (Datalog.Program.to_abstract prog) ;
Log.info (fun m -> m "That's all.");
let dist_type_image = interpret_type dist_type lex in
let term =
Lambda.normalize
~id_to_term:(fun i -> Sg.unfold_term_definition i lex.object_sig)
(Signature.expand_term term lex.object_sig) in
LOG "Term for the query: %s" (Signature.term_to_string term lex.object_sig) LEVEL DEBUG;
Log.info (fun m -> m "Term for the query: %s" (Signature.term_to_string term lex.object_sig));
let obj_term=
Sg.eta_long_form
term
dist_type_image
lex.object_sig in
let obj_princ_type,obj_typing_env = TypeInference.Type.inference obj_term in
LOG "Going to set a query for the distinguised type \"%s(%s)\"" (Signature.type_to_string dist_type lex.abstract_sig) (Lambda.raw_type_to_string dist_type) LEVEL DEBUG;
LOG "whose image is \"%s(%s)\"" (Signature.type_to_string dist_type_image lex.object_sig) (Lambda.raw_type_to_string dist_type_image) LEVEL DEBUG;
LOG "resulting int the principle type \"%s\"" (Lambda.raw_type_to_string obj_princ_type) LEVEL DEBUG;
Log.debug (fun m -> m "Going to set a query for the distinguised type \"%s(%s)\"" (Signature.type_to_string dist_type lex.abstract_sig) (Lambda.raw_type_to_string dist_type));
Log.debug (fun m -> m "whose image is \"%s(%s)\"" (Signature.type_to_string dist_type_image lex.object_sig) (Lambda.raw_type_to_string dist_type_image));
Log.debug (fun m -> m "resulting int the principle type \"%s\"" (Lambda.raw_type_to_string obj_princ_type));
let query,temp_prog =
Reduction.edb_and_query
~obj_term
......@@ -311,24 +314,15 @@ struct
prog
~abs_sig:lex.abstract_sig
~obj_sig:lex.object_sig in
LOG "Going to solve the query: \"%s\" with the program:" (DatalogAbstractSyntax.Predicate.to_string query temp_prog.Datalog.Program.pred_table temp_prog.Datalog.Program.const_table) LEVEL TRACE;
LOG "%s"
(let buff'=Buffer.create 80 in
let () = Buffer.add_buffer
buff'
(DatalogAbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract temp_prog)) in
let () = Utils.log_iteration
(fun s -> LOG s LEVEL TRACE)
(Buffer.contents buff') in "")
LEVEL DEBUG;
Log.info (fun m -> m "Going to solve the query: \"%s\" with the program:" (DatalogAbstractSyntax.Predicate.to_string query temp_prog.Datalog.Program.pred_table temp_prog.Datalog.Program.const_table));
DatalogAbstractSyntax.Program.log_content Logs.Debug (Datalog.Program.to_abstract temp_prog);
let starting_parse_time = Sys.time () in
let derived_facts,derivations = Datalog.Program.seminaive temp_prog in
let ending_parse_time = Sys.time () in
let parse_forest = Datalog.Program.build_forest ~query:query derivations temp_prog in
let ending_building_forest_time = Sys.time () in
(* let () = Printf.printf "Pre-parsing time: %.3f seconds\n%!" (starting_parse_time -. pre_parse_time) in *)
let () = Printf.printf "Parsing time: %.3f seconds\n%!" (ending_parse_time -. starting_parse_time) in
let () = Printf.printf "Building forest time: %.3f seconds\n%!" (ending_building_forest_time -. ending_parse_time) in
let () = Logs.app (fun m -> m "Parsing time: %.3f seconds\n%!" (ending_parse_time -. starting_parse_time)) in
let () = Logs.app (fun m -> m "Building forest time: %.3f seconds\n%!" (ending_building_forest_time -. ending_parse_time)) in
let resume =
match parse_forest with
| [] -> SharedForest.SharedForest.empty
......@@ -339,20 +333,19 @@ struct
resume
| Some _ , _ ->
let () =
Printf.printf "Parsing is not yet implemented for non atomic distinguished type\n%!" in
Logs.warn (fun m -> m "Parsing is not yet implemented for non atomic distinguished type") in
SharedForest.SharedForest.empty
let get_analysis resume lex =
LOG "Trying to get some analysis" LEVEL DEBUG;
Log.debug (fun m -> m "Trying to get some analysis");
match lex.datalog_prog with
| None -> let () = Printf.printf "Parsing is not yet implemented for non atomic distinguished type\n%!" in None,resume
(* | Some (_,rule_id_to_cst) -> *)
| None -> let () = Logs.warn (fun m -> m "Parsing is not yet implemented for non atomic distinguished type\n%!") in None,resume
| Some {rule_to_cst=rule_id_to_cst} ->
match SharedForest.SharedForest.resumption resume with
| None,resume -> None,resume
| Some t,resume ->
LOG "Got a result. Ready to map it" LEVEL DEBUG;
Log.debug (fun m -> m "Got a result. Ready to map it");
Some (SharedForest.SharedForest.fold_depth_first
((fun rule_id -> RuleToCstMap.find rule_id rule_id_to_cst),
(fun x y -> Lambda.App(x,y)))
......@@ -427,7 +420,7 @@ struct
{new_lex with timestamp=Unix.time ()}
let compose lex1 lex2 n =
LOG "Compose %s(%s) as %s" (fst(name lex1)) (fst(name lex2)) (fst n) LEVEL TRACE;
Log.info (fun m -> m "Compose %s(%s) as %s" (fst(name lex1)) (fst(name lex2)) (fst n));
let temp_lex=
{name=n;
dico =
......
......@@ -5,10 +5,6 @@
(name acgData)
(public_name acgtkLib.acgData)
(flags (:standard -w -58))
(preprocess (per_module
((action (system "%{bin:camlp4} -parser o -parser op -printer a -loc loc %{lib:bolt:bolt_pp.cmo} -level NONE %{input-file}" ))
reduction acg_lexicon type_system signature)
))
(libraries
logic ; internal library
datalogLib ; internal library
......
......@@ -6,6 +6,10 @@ open DatalogLib.Datalog
module Make(Sg:Interface.Signature_sig with type term = Lambda.term and type stype = Lambda.stype) =
struct
let src = Logs.Src.create "ACGtkLib.reduction" ~doc:"logs ACGtkLib reduction events"
module Log = (val Logs.src_log src : Logs.LOG)
let rec sequentialize_rev stype sequence =
match stype with
| Lambda.Atom i -> i::sequence
......@@ -26,8 +30,8 @@ struct
let map_types abs_type obj_type sg =
let rec map_types_aux abs_type obj_type lst =
LOG "Mapping (aux) type:%s" (Sg.type_to_string abs_type sg) LEVEL TRACE;
LOG "On (aux): %s" (Lambda.raw_type_to_string obj_type) LEVEL TRACE;
Log.debug (fun m -> m "Mapping (aux) type:%s" (Sg.type_to_string abs_type sg));
Log.debug (fun m -> m "On (aux): %s" (Lambda.raw_type_to_string obj_type));
match abs_type,obj_type with
| Lambda.Atom i,_ -> (i,Sg.type_to_string abs_type sg,obj_type)::lst
| Lambda.DAtom _,_ -> failwith (Printf.sprintf "Bug: type definition in \"%s\" as \"%s\" should be unfolded" (Sg.type_to_string abs_type sg) (Lambda.raw_type_to_string abs_type))
......@@ -37,8 +41,8 @@ struct
| Lambda.LFun _,Lambda.Fun _
| Lambda.Fun _,Lambda.Fun _ -> failwith "Bug: should be 2nd order type for abstract constant"
| _,_ -> failwith "Bug: Not a 2nd order type or not corresponding abstract and object type" in
LOG "Mapping type:%s (%s)" (Sg.type_to_string abs_type sg) (Lambda.raw_type_to_string abs_type) LEVEL TRACE;
LOG "On: %s" (Lambda.raw_type_to_string obj_type) LEVEL TRACE;
Log.debug (fun m -> m "Mapping type:%s (%s)" (Sg.type_to_string abs_type sg) (Lambda.raw_type_to_string abs_type));
Log.debug (fun m -> m "On: %s" (Lambda.raw_type_to_string obj_type));
map_types_aux abs_type obj_type []
......@@ -60,7 +64,7 @@ struct
*)
let build_predicate_w_var_args (name,obj_type) (prog,var_gen,type_to_var_map) =
let atom_sequence = sequentialize_rev obj_type [] in
LOG "Build predicate from %s:%s ([%s])" name (Lambda.raw_type_to_string obj_type) (string_of_list ";" string_of_int atom_sequence) LEVEL TRACE;
Log.debug (fun m -> m "Build predicate from %s:%s ([%s])" name (Lambda.raw_type_to_string obj_type) (string_of_list ";" string_of_int atom_sequence));
let var_sequence,var_gen,type_to_var_map =
List.fold_left
(fun (l_var_seq,l_var_gen,l_type_to_var_map) i ->
......@@ -88,7 +92,7 @@ struct
*)
let build_predicate_w_cst_args (name,obj_type) prog =
let atom_sequence = sequentialize obj_type in
LOG "Build predicate from %s:%s ([%s])" name (Lambda.raw_type_to_string obj_type) (string_of_list ";" string_of_int atom_sequence) LEVEL TRACE;
Log.debug (fun m -> m "Build predicate from %s:%s ([%s])" name (Lambda.raw_type_to_string obj_type) (string_of_list ";" string_of_int atom_sequence));
let const_sequence,prog =
List.fold_left
(fun (l_const_seq,l_prog) i ->
......@@ -149,7 +153,7 @@ struct
(new_pred,l_length)::rhs,l_length,new_tables)
env
([],0,(prog,var_gen,type_to_var_map) ) in
LOG "Correctly set the number of intensional predi in rhs: %d" (let () = assert (length=List.length i_rhs) in length) LEVEL DEBUG;
Log.debug (fun m -> m "Correctly set the number of intensional predi in rhs: %d" (let () = assert (length=List.length i_rhs) in length));
let new_rule = AbstractSyntax.Rule.({id=rule_id;lhs;e_rhs;i_rhs;i_rhs_num=length}) in
new_rule,Datalog.Program.add_rule ~intensional:true new_rule prog
......
......@@ -28,7 +28,7 @@ type sig_entry =
| Term_declaration of string * int * Abstract_syntax.syntactic_behavior * Lambda.stype
| Term_definition of string * int * Abstract_syntax.syntactic_behavior * Lambda.stype * Lambda.term
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.signature" ~doc:"logs ACGtkLib signature events") : Logs.LOG)
module Make(Symbols:TABLE with type key=String.t)(Id:TABLE with type key=int) =
struct
......@@ -228,8 +228,8 @@ struct
let expanded_type= expand_type stype sg in
let expanded_term= expand_term term sg in
let res = Lambda.eta_long_form expanded_term expanded_type (fun id -> get_type_of_const_id id sg) in
LOG "term: %s:%s" (term_to_string term sg) (type_to_string stype sg) LEVEL TRACE;
LOG "eta_long_form: %s:%s" (term_to_string res sg) (type_to_string expanded_type sg) LEVEL TRACE;
Log.debug (fun m -> m "term: %s:%s" (term_to_string term sg) (type_to_string stype sg));
Log.debug (fun m -> m "eta_long_form: %s:%s" (term_to_string res sg) (type_to_string expanded_type sg));
res
......
......@@ -28,7 +28,8 @@ let get_location = function
| Abstract_syntax.LAbs (_,_,_,l) -> l
| Abstract_syntax.App (_,_,l) -> l
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.type_system" ~doc:"logs ACGtkLib type_system events") : Logs.LOG)
module type SIG_ACCESS =
sig
exception Not_found
......@@ -294,9 +295,9 @@ struct
try
let t_term,t_type,(_:typing_environment) =
typecheck_aux t (Some (local_expand ty)) {linear_level=0;level=0;env=Utils.StringMap.empty;wrapper=None} in
LOG "Type-checked %s : %s" (Signature.term_to_string t_term sg ) (Signature.type_to_string t_type sg ) LEVEL TRACE ;
LOG "Type-checked %s : %s" (Lambda.raw_to_string t_term ) (Lambda.raw_type_to_string t_type ) LEVEL TRACE ;
LOG "Type-checked %s : %s" (Lambda.raw_to_caml t_term ) (Lambda.raw_type_to_caml t_type ) LEVEL TRACE ;
Log.debug (fun m -> m "Type-checked %s : %s" (Signature.term_to_string t_term sg ) (Signature.type_to_string t_type sg ));
Log.debug (fun m -> m "Type-checked %s : %s" (Lambda.raw_to_string t_term ) (Lambda.raw_type_to_string t_type ));
Log.debug (fun m -> m "Type-checked %s : %s" (Lambda.raw_to_caml t_term ) (Lambda.raw_type_to_caml t_type ));
t_term
with
| Type_mismatch ((p1,p2),t1,t2) -> raise (Error.Error (Error.Type_error (Error.Is_Used (Signature.type_to_string t1 sg,Printf.sprintf "\"%s\"" (Signature.type_to_string t2 sg)),(p1,p2))))
......
......@@ -20,3 +20,5 @@ Full parse lambda z. a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a
# a^40 b^40 c^40 d^39
Full parse lambda z. a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(a(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(b(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(c(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d(d z)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) : S;
exit;
\ No newline at end of file
This diff is collapsed.
......@@ -27,7 +27,10 @@ end
module ConstGen=IdGen(Const)
module AbstractSyntax =
struct
struct
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.datalog_AbstractSyntax" ~doc:"logs ACGtkLib datalog_AbstractSyntax events") : Logs.LOG)
(** These modules are the abstract syntactic representations of the
predicates, of the rules, and of the programs *)
module Predicate =
......@@ -406,6 +409,16 @@ struct
(fun elt -> Buffer.add_string buff (Printf.sprintf "\t%s\n%!" (Predicate.PredIdTable.find_sym_from_id elt prog.pred_table)))
prog.i_preds in
buff
let log_content level prog =
let () = Log.msg level (fun m -> m "Intensional predicates are:") in
Log.msg level (fun m ->
let () = Predicate.PredIds.iter
(fun elt -> Log.msg level (fun m -> m "\t%s" (Predicate.PredIdTable.find_sym_from_id elt prog.pred_table)))
prog.i_preds in
m "Done.")
end
end
......
......@@ -115,6 +115,7 @@ sig
val make_program : Proto_Program.t -> program
val extend : program -> Proto_Program.t -> program
val to_buffer : program -> Buffer.t
val log_content : Logs.level -> program -> unit
end
end
......
......@@ -28,45 +28,43 @@ let parse_file query edb filename =
let fullname = UtilsLib.Utils.find_file filename [""] in
open_in fullname in
let lexbuf = Lexing.from_channel in_ch in
LOG "Parsing \"%s\"..." filename LEVEL INFO;
Logs.app (fun m -> m "Parsing \"%s\"..." filename);
let prog=DatalogLib.Db_parser.program DatalogLib.Db_lexer.lexer lexbuf AbstractSyntax.Proto_Program.empty in
LOG "Done." LEVEL INFO;
LOG "Current symbol tables:" LEVEL DEBUG ;
UtilsLib.Utils.log_iteration
(fun s -> LOG s LEVEL DEBUG)
(AbstractSyntax.Predicate.PredIdTable.to_string prog.AbstractSyntax.Proto_Program.pred_table);
Logs.app (fun m -> m "Done.");
Logs.debug (fun m -> m "Current symbol tables:");
AbstractSyntax.Predicate.PredIdTable.log_content Logs.Debug prog.AbstractSyntax.Proto_Program.pred_table;
let sep=String.make 15 '*' in
let () = Printf.printf "%s\n%!" sep in
let () = Printf.printf "Create the abstract program and print it...\n" in
Logs.app (fun m -> m "%s%!" sep);
Logs.app (fun m -> m "Create the abstract program and print it...");
let abs_program = AbstractSyntax.Program.make_program prog in
let () = Buffer.output_buffer stdout (AbstractSyntax.Program.to_buffer abs_program) in
let () = Printf.printf "Done.\n" in
let () = Printf.printf "%s\n" sep in
let () = Printf.printf "Create the internal program and print it...\n" in
Logs.app (fun m -> m "Done.");
Logs.app (fun m -> m "%s" sep);
Logs.app (fun m -> m "Create the internal program and print it...");
let program=Datalog.Program.make_program abs_program in
let () = Buffer.output_buffer stdout (AbstractSyntax.Program.to_buffer (Datalog.Program.to_abstract program)) in
let () = Printf.printf "Done.\n" in
let () = Printf.printf "%s\n" sep in
Logs.app (fun m -> m "Done.");
Logs.app (fun m -> m "%s" sep);
let program =
match edb with
| None ->
LOG "I didn't find an edb file to parse." LEVEL DEBUG ;
Logs.debug (fun m -> m "I didn't find an edb file to parse.");
program
| Some edb_filename ->
LOG "I found an edb file to parse." LEVEL DEBUG ;
Logs.debug (fun m -> m "I found an edb file to parse.");
let edb_in_ch =
let edb_fullname = UtilsLib.Utils.find_file edb_filename [""] in
open_in edb_fullname in
let edb_lexbuf = Lexing.from_channel edb_in_ch in
LOG "Parsing \"%s\"..." edb_filename LEVEL INFO;
Logs.app (fun m -> m "Parsing \"%s\"..." edb_filename);
let to_be_added=DatalogLib.Db_parser.extensional_facts DatalogLib.Db_lexer.lexer edb_lexbuf Datalog.Program.(program.pred_table,program.const_table,program.rule_id_gen) in
LOG "Done." LEVEL INFO;
Logs.app (fun m -> m "Done.");
Datalog.Program.add_e_facts program to_be_added in
let derived_facts,derivations = Datalog.Program.seminaive program in
let () = Printf.printf "I could derive the following facts:\n%s\n" (Datalog.Predicate.facts_to_string derived_facts program.Datalog.Program.pred_table program.Datalog.Program.const_table) in
Logs.app (fun m -> m "I could derive the following facts:\n%s" (Datalog.Predicate.facts_to_string derived_facts program.Datalog.Program.pred_table program.Datalog.Program.const_table));
let buff = Buffer.create 80 in
let () = Datalog.Predicate.add_map_to_premises_to_buffer buff program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations in
let () = Printf.printf "With the following derivations:\n%s\n" (Buffer.contents buff) in
Logs.app (fun m -> m "With the following derivations:\n%s\n" (Buffer.contents buff));
let query,new_pred_table,new_cons_table =
match query with
| None ->
......@@ -75,7 +73,7 @@ let parse_file query edb filename =
let q,t1,t2=DatalogLib.Db_parser.query DatalogLib.Db_lexer.lexer (Lexing.from_string s) Datalog.Program.(program.pred_table,program.const_table) in
Some q,t1,t2 in
let () = Datalog.Predicate.format_derivations2 ?query:query program.Datalog.Program.pred_table program.Datalog.Program.const_table derivations in
let () = Printf.printf "%s\n" (Buffer.contents (Format.stdbuf)) in
Logs.app (fun m -> m "%s" (Buffer.contents (Format.stdbuf)));
()
......@@ -87,8 +85,11 @@ let query=ref None
let options =
[
("-edb",Arg.String (fun s -> edb_file:=Some s),"Add the specified file as an edb (it should include only extensional facts).");
("-q",Arg.String (fun s -> query:=Some s),"Only outputs the derivations satisfyin the specified query")
("-q",Arg.String (fun s -> query:=Some s),"Only outputs the derivations satisfying the specified query")
]
let () =
Arg.parse options (fun s -> parse_file !query !edb_file s) usage_msg
let () = UtilsLib.Log.set_level Logs.Debug in
if Array.length (Sys.argv) > 1 then
Arg.parse options (fun s -> parse_file !query !edb_file s) usage_msg
else parse_file None None "/home/pogodall/work/dev/ACGtk/src/datalog.prover/Jean-regarde-telescope.dl"
......@@ -8,14 +8,6 @@
(name datalogLib)
(public_name acgtkLib.datalogLib)
(flags (:standard -w -58))
(preprocess (per_module
(
(action (system "%{bin:camlp4} -parser o -parser op -printer a -loc loc %{lib:bolt:bolt_pp.cmo} -level NONE %{input-file}" ))
datalog
unionFind
)
)
)
(modules (:standard db_parser db_lexer \ test db_test))
(libraries
bolt ; external libraries
......@@ -24,21 +16,15 @@
utilsLib ; internal library
))
(executables
(tests
(names test db_test)
(modules test db_test)
(preprocess (per_module
((action (system "%{bin:camlp4} -parser o -parser op -printer a -loc loc %{lib:bolt:bolt_pp.cmo} -level NONE %{input-file}" ))
db_test)
))
(libraries
threads
fmt.tty
utilsLib
datalogLib
))
(alias
(name testbuild)
(deps test.exe db_test.exe))
(documentation (package acgtk))
......@@ -74,6 +74,7 @@ let () =
let () = print_newline()
let () =
let () = UtilsLib.Log.set_level Logs.Debug in
OddIntArray.collect_results
(fun _ res -> Printf.printf "State: %s\n%!" (string_of_res res))
()
......
......@@ -70,8 +70,11 @@ sig
val copy : 'a t -> 'a t
val to_string : 'a t -> string
val log_content : Logs.level -> 'a t -> unit
end
module Log = (val Logs.src_log (Logs.Src.create "ACGtkLib.unionFind" ~doc:"logs ACGtkLib unionFind events") : Logs.LOG)
(** Modules with this module type should provide an indexed (by [int]
indexes) storage data structure for ['a] type values and access
and update functions.
......@@ -145,7 +148,29 @@ struct
"Bug!"
with
| S.Store_Not_found -> Buffer.contents buff
let log_content level {rank=r;parents=p} =
Log.msg
level
(fun m ->
let log_content_aux i =
let content = (content_to_string (S.get i p)) in
let rk = S.get i r in
Log.msg level (fun m -> m "%d\t<--->\t%s\t\t(%d)" i content rk) in
let i=ref 1 in
let () =
try
let () =
while true do
log_content_aux !i;
i:=!i+1
done in
()
with
| S.Store_Not_found -> () in
m "Done.")
(* Indexing starts at 1, not at 0 *)
......@@ -158,10 +183,10 @@ struct
let res,_=
List.fold_left
(fun ({rank=r;parents=p},k) content ->
LOG "Setting the following content at address %d:" k LEVEL DEBUG;
Log.debug (fun m -> m "Setting the following content at address %d:" k);
match content with
| Link_to i as c ->
LOG "Link to %d" i LEVEL DEBUG;
Log.debug (fun m -> m "Link to %d" i);
(* rank is unset for contents that are initially a link *)
({rank=
(try
......@@ -171,7 +196,7 @@ struct
| S.Store_Not_found -> S.set i 1 r);
parents=S.set k c p},k+1)
| Value v as c ->
LOG "Some value" LEVEL DEBUG;
Log.debug (fun m -> m "Some value");
({rank=
(try
let _ = S.get k r in
......@@ -182,9 +207,12 @@ struct
(* ({rank=S.empty ln;parents=S.empty ln},1) *)
({rank=S.make ln 0;parents=S.make ln (Link_to (-1))},1)
contents in
for i = 1 to ln do
LOG "%d/%d\t<--->\t%s\t\t(%d)" i ln (content_to_string (S.get i res.parents)) (S.get i res.rank) LEVEL TRACE;
done;
Log.debug (fun m ->
let () =
for i = 1 to ln do
Log.debug (fun m -> m "%d/%d\t<--->\t%s\t\t(%d)" i ln (content_to_string (S.get i res.parents)) (S.get i res.rank));
done in
m "Done.");
res
......@@ -194,17 +222,17 @@ struct
to be a variable, not an actual value. It also performs path
compression *)
let rec find_aux i f =
LOG "Extracting %d" i LEVEL TRACE;
LOG "find_aux work with the following content:" LEVEL TRACE;
Log.debug (fun m -> m "Extracting %d" i);
Log.debug (fun m -> m "find_aux work with the following content:");
(* ATTENTION: To be removed when optimizing *)
LOG "%s"
(let () =
let i'=ref 1 in
while !i' <= (S.length f) do
LOG "%d\t<--->\t%s" !i' (content_to_string (S.get !i' f)) LEVEL TRACE;
i':=!i'+1
done in
"Done.") LEVEL TRACE;
Log.debug (fun m ->
let i'=ref 1 in
let () =
while !i' <= (S.length f) do
Log.debug (fun m -> m "%d\t<--->\t%s" !i' (content_to_string (S.get !i' f)));
i':=!i'+1
done in
m "Done.");
match S.get i f with
| Value _ as v -> (i,v),f
(* An actual value was reached at index [i]. So [i] is returned
......@@ -219,12 +247,11 @@ struct
(* Then we update the storage data structure linking the context
indexed by [i] directly to the representative index *)
let updated_f = S.set i (Link_to representative_index) new_f in
LOG "the \"UnionFinf.find\" function indeed returns a Link_to itself: %b"
(
let ()=match representative_value with
| Link_to variable -> assert (representative_index=variable)
| _ -> () in true)
LEVEL FATAL;
Log.debug (fun m -> m "the \"UnionFinf.find\" function indeed returns a Link_to itself: %B"
(
let ()=match representative_value with
| Link_to variable -> assert (representative_index=variable)
| _ -> () in true));
(representative_index,representative_value),updated_f
(** [find i h] returns a pair [(i',v),f'] where [i'] is the index of
......@@ -235,7 +262,7 @@ struct
to the whole storage data structure (that includes data for
weighted union). *)
let find i h =
LOG "find is about to call find_aux with the following content:" LEVEL TRACE;
Log.debug (fun m -> m "find is about to call find_aux with the following content:");
let rep_i,f = find_aux i h.parents in
rep_i,{h with parents=f}
......@@ -245,8 +272,9 @@ struct
values of representatives (i.e it follows the [Link_to] links
until the value of the representative before returning it). *)
let extract ?(start=1) i content =
LOG "Going to extract %d elements starting at %d..." i start LEVEL DEBUG;
LOG "Done.%s" (let () = log_iteration (fun s -> LOG s LEVEL TRACE) (to_string content) in "") LEVEL TRACE;
Log.debug (fun m -> m "Going to extract %d elements starting at %d..." i start);
log_content Logs.Debug content;
Log.debug (fun m -> m "Done.");
let rec extract_aux k res =
match k-