Skip to content
Projects
Groups
Snippets
Help
Loading...
Help
Support
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
A
ACGtk
Project overview
Project overview
Details
Activity
Releases
Cycle Analytics
Repository
Repository
Files
Commits
Branches
Tags
Contributors
Graph
Compare
Charts
Issues
7
Issues
7
List
Boards
Labels
Milestones
Merge Requests
0
Merge Requests
0
Packages
Packages
Container Registry
Wiki
Wiki
Snippets
Snippets
Members
Members
Collapse sidebar
Close sidebar
Activity
Graph
Charts
Create a new issue
Commits
Issue Boards
Open sidebar
ACG
dev
ACGtk
Commits
31fee9e7
Commit
31fee9e7
authored
Jun 16, 2014
by
POGODALLA Sylvain
Browse files
Options
Browse Files
Download
Email Patches
Plain Diff
Added some comments
parent
c3b1af05
Changes
3
Hide whitespace changes
Inline
Side-by-side
Showing
3 changed files
with
105 additions
and
6 deletions
+105
-6
TODO
TODO
+12
-0
src/acg-data/reduction.ml
src/acg-data/reduction.ml
+58
-4
src/acg-data/reduction.mli
src/acg-data/reduction.mli
+35
-2
No files found.
TODO
View file @
31fee9e7
...
...
@@ -8,6 +8,8 @@
+ [X] réfléchir si changement de construction des numéros de version
+ [X] renommer s_datalog et datalog en datalog.prover et datalog.solver
+ [X] modifier la documentation
+ [ ] remove useless reduction.* files (hint: the useful one is in the
acg-data directory)
** DONE Faire un Bolt package
...
...
@@ -21,6 +23,11 @@
** DONE Configuration
+ [X] Utiliser les outils de Paul
** Optimisation
+ [ ] magic rewriting
+ [ ] PersistentArray
+ [ ] paralélisme
** Permettre l'utilisation des PersistentArray
** TODO Vérifier (et supprimer ou mettre en IFDEBUG) les assert
...
...
@@ -56,6 +63,11 @@
+ [ ] changer edb et idb en Set plutôt que list
+ [ ] build_forest sans query n'est pas correct (il faut faire
plusieurs forêts)
* reduction.ml
+ [ ] offrir la possibilité de construire une requête à partir de plusieurs terms
+ [ ] offrir la possibilité de construire une requête non totalement
instanciée (utile ?). Prévoir modifications dans la manière de
construire la forêt partagée après une requête.
* alterTrees.ml
+ [ ] changer la focused list des forêts en simple liste ?
...
...
src/acg-data/reduction.ml
View file @
31fee9e7
...
...
@@ -41,6 +41,22 @@ struct
map_types_aux
abs_type
obj_type
[]
(** [build_predicate_w_var_args (name,obj_type)
(prog,var_gen,type_to_var_map)] returns [(prog',var_gen',type_to_var_map')] where:
- [name] is the name of an abstract type of some ACG that
has to be turned into a predicate of the associated datalog
program
- [ob_type] is the principal type of its realisation by this ACG
- [prog] is the current associated datalog program
- [var_gen] is a variable generator that records the variable
associated with this predicate (according to the principal type
[obj_type] of its image). It can be updated to [var_gen'] if
some new variables are needed
- [type_to_var_map] records to which variable each atomic type
of the principal type is associated with. It can be updated to
[type_to_var_map'] if some new variables were needed.
- [prog'] is [prog] where the bew predicate has been added
*)
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
)
(
Utils
.
string_of_list
";"
string_of_int
atom_sequence
)
LEVEL
TRACE
;
...
...
@@ -61,7 +77,14 @@ struct
AbstractSyntax
.
Predicate
.({
p_id
=
p_id
;
arity
=
List
.
length
var_sequence
;
arguments
=
var_sequence
})
,
(
prog
,
var_gen
,
type_to_var_map
)
(** [build_predicate_w_cst_args (name,obj_type) prog] returns a fully instantiated predicate where:
- [name] is the name of an abstract type of some ACG that has to
be turned into a the querying predicate for the associated
datalog program
- [ob_type] is the principal type of its realisation by this ACG
that is interpreted as Datalog constants
- [prog] is the current associated datalog program
*)
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
)
(
Utils
.
string_of_list
";"
string_of_int
atom_sequence
)
LEVEL
TRACE
;
...
...
@@ -76,6 +99,22 @@ struct
AbstractSyntax
.
Predicate
.({
p_id
=
p_id
;
arity
=
List
.
length
const_sequence
;
arguments
=
List
.
rev
const_sequence
})
,
prog
(** [generate_and_add_rule ~abs_cst ~obj_princ_type ~obj_typing_env
prog abs_sig obj_sig] returns a pair [(r,prog')] where:
- [r] is the generated rule
- [prog'] is [prog] where the rule [r] has been added
- [abs_cst] is the abstract constant from the abstract signature
[abs_sig] that triggers the rule generation
- [obj_princ_type] is the principal type of the image by the
lexicon of [abs_cst]
- [obj_typing_env] is its typing environment. The latter maps
the position of the object constants in the realisation of
[abs_cst] to a pair [(t,ty)] where [t] is the object constant
itself, and [ty] the type associated by the principal typing
environment.
- [prog] is the current datalog program
- [abs_sig] and [obj_sig] are the abstract signature and the
object signature of some ACG. *)
let
generate_and_add_rule
~
abs_cst
:
(
name
,
abs_t_type
)
...
...
@@ -113,10 +152,25 @@ struct
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
(* It makes the assumption that no constant has been
(** [edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type
prog ~abs_sig ~obj_sig] returns a pair [(q,prog')] where:
- [q] is the predicate corresponding to the query generated by
the object term [obj_term] to parse
- [prog'] is [prog] where the extensional database resulting
from the reduction of the object term [obj_term]
- [obj_type] is the principal type of [obj_term]
- [obj_typing_env] is its typing environment. The latter maps
the position of the object constants in the realisation of
[abs_cst] to a pair [(t,ty)] where [t] is the object constant
itself, and [ty] the type associated by the principal typing
environment.
- [dist_type] is the distinguished type of the ACG
- [prog] is the current datalog program
- [abs_sig] and [obj_sig] are the abstract signature and the
object signature of some ACG. *)
let
edb_and_query
~
obj_term
~
obj_type
~
obj_typing_env
~
dist_type
prog
~
abs_sig
~
obj_sig
=
(* It makes the assumption that no constant has been
previously defined or used in the program *)
let
edb_and_query
~
obj_term
~
obj_type
~
obj_typing_env
~
dist_type
prog
~
abs_sig
~
obj_sig
=
let
type_lst
=
map_types
dist_type
obj_type
abs_sig
obj_sig
in
match
type_lst
with
|
[]
->
failwith
"Bug: there should be a type correspondance"
...
...
src/acg-data/reduction.mli
View file @
31fee9e7
open
Datalog_AbstractSyntax
(** This module implements the reduction from ACG signatures and
lexicons to datalog programs *)
module
Make
(
Sg
:
Interface
.
Signature_sig
with
type
term
=
Lambda
.
Lambda
.
term
and
type
stype
=
Lambda
.
Lambda
.
stype
)
:
sig
(** [generate_and_add_rule ~abs_cst ~obj_princ_type ~obj_typing_env
prog abs_sig obj_sig] returns a pair [(r,prog')] where:
- [r] is the generated rule
- [prog'] is [prog] where the rule [r] has been added
- [abs_cst] is the abstract constant from the abstract signature
[abs_sig] that triggers the rule generation
- [obj_princ_type] is the principal type of the image by the
lexicon of [abs_cst]
- [obj_typing_env] is its typing environment. The latter maps
the position of the object constants in the realisation of
[abs_cst] to a pair [(t,ty)] where [t] is the object constant
itself, and [ty] the type associated by the principal typing
environment.
- [prog] is the current datalog program
- [abs_sig] and [obj_sig] are the abstract signature and the
object signature of some ACG. *)
val
generate_and_add_rule
:
abs_cst
:
(
string
*
Lambda
.
Lambda
.
stype
)
->
obj_princ_type
:
Lambda
.
Lambda
.
stype
->
...
...
@@ -12,7 +30,22 @@ sig
obj_sig
:
Sg
.
t
->
(
AbstractSyntax
.
Rule
.
rule
*
Datalog
.
Datalog
.
Program
.
program
)
(** [edb_and_query ~obj_term ~obj_type ~obj_typing_env ~dist_type
prog ~abs_sig ~obj_sig] returns a pair [(q,prog')] where:
- [q] is the predicate corresponding to the query generated by
the object term [obj_term] to parse
- [prog'] is [prog] where the extensional database resulting
from the reduction of the object term [obj_term]
- [obj_type] is the principal type of [obj_term]
- [obj_typing_env] is its typing environment. The latter maps
the position of the object constants in the realisation of
[abs_cst] to a pair [(t,ty)] where [t] is the object constant
itself, and [ty] the type associated by the principal typing
environment.
- [dist_type] is the distinguished type of the ACG
- [prog] is the current datalog program
- [abs_sig] and [obj_sig] are the abstract signature and the
object signature of some ACG. *)
val
edb_and_query
:
obj_term
:
Lambda
.
Lambda
.
term
->
obj_type
:
Lambda
.
Lambda
.
stype
->
...
...
Write
Preview
Markdown
is supported
0%
Try again
or
attach a new file
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment