Commit fd4399db authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

Fix some left dependencies to bolt. First steps towards using menhir instead of dypgen.

parent db02e6b3
......@@ -48,38 +48,14 @@ end
** TODO Avant Prochaine release
+ [X] merge avec trunk
+ [X] remplacer tous les gforge.loria en gforge.inria
+ [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
+ [X] remove useless reduction.* files (hint: the useful one is in the
acg-data directory)
+ [X] améliorer le pretty-printing des termes
+ [X] ajouter dépendence à ocf
+ [X] ajouter dépendence à Ocaml 4.02.1 ? (requis par ocf)
+ [ ] ajouter parsing de types non atomiques
+ [ ] ajouter détection de nbre infini de solutions
+ [ ] permettre à ./acg de charger des fichiers .acgo
+ [X] OPAM: enlever les warnings qui deviennent des erreurs
+ [ ] utiliser UF avec tableaux destructifs, et tester l'amélioration des performances
+ [ ] autoriser l'utilisation de symboles non fonctionnels
+ [ ] enlever les dépendences à yojson.cmo et à eay-format.cmo dans scripting/Makefile.in, les remplacer par .cma
+ [ ] refaire la compilation du projet avec ocamlbuild/oasis/ocamlfind
+ [ ] rajouter l'utf8
+ [ ] générer svg aussi pour la commande parse
** DONE Faire un Bolt package
** DONE Utiliser Bolt (http://bolt.x9c.fr/)
+ [X] Intégrer dans le configure.ac la dépendance à Bolt
+ [X] Laisser la possibilité que la librairie ne soit pas installée *Impossible*
+ [X] Gérer la présence d'un fichier bolt_config (bolt.config) (DONE:
bug fix in BOLT)
** DONE Configuration
+ [X] Utiliser les outils de Paul
+ [ ] Uniformiser les sorties avec logs
** Optimisation
+ [ ] magic rewriting
......@@ -91,17 +67,6 @@ end
** TODO Vérifier (et supprimer ou mettre en IFDEBUG) les assert
** TODO Avant merge et prochaine release :
+ [X] mettre la commande "analyse" en deprecated
+ [X] la remplacer par
+ [X] une commande "check"
+ [X] une commande "realise"
+ [X] mettre une commande "idb"
+ [X] mettre une commande "query"
+ [X] vérifier que tous les "help cmd" fonctionnent
** lexer and parser
+ [ ] change the compilation order and the token emission
* datalog.ml
+ [ ] Vérifier pourquoi "pred_table" est paramètre de Rule.to_abstract
......@@ -153,21 +118,15 @@ end
* acg_lexicon.ml
+ [X] rebuild the datalog program after composition
+ [ ] add the int id (as in Lambda.Const i) in the map from the
constant name for abstract constants
+ [X] Définir le parsing de la composition de lexique
+ [ ] Définir le parsing pour les types non atomiques
+ [ ] Définir le parsing pour les almost linear terms
+ [ ] Vérifier que les Signature.expand_term ne sont pas redondants
avec les Lambda.normalize ~id_to_term
* Divers
+ [X] ajouter la commande compose dans les fichiers de définition de
lexiques et signature
+ [ ] ajouter un espace de nommage pour les lexiques et signatures
+ [X] faire des dumps des interfaces et des représentations binaires
pour charger plus vite
+ [ ] Ajouter un -nooout option pour acgc ?
+ [ ] Vérifier ce qui se passe avec les différents parenthèsages lors
du parsing
......
This diff is collapsed.
(lang dune 1.0)
\ No newline at end of file
(lang dune 1.0)
(using menhir 1.0)
......@@ -55,11 +55,17 @@ type parse_error =
| Duplicated_type of string
| Binder_expected of string
| Unknown_constant of string
| Unknown_constant_nor_variable of string
| Unknown_constant_nor_type of string
| Unknown_type of string
| Missing_arg_of_Infix of string
| No_such_signature of string
| No_such_lexicon of string
| Dyp_error
| Not_associative of string
| Not_infix of string
| Prefix_missing_arg of string
| Infix_missing_first_arg of string
| Infix_missing_second_arg of string
type type_error =
| Already_defined_var of string
......@@ -103,7 +109,7 @@ type error =
type warning =
| Variable_or_constant of (string * Lexing.position * Lexing.position)
| Variable_or_constant of (string * (Lexing.position * Lexing.position))
exception Error of error
......@@ -133,11 +139,17 @@ let parse_error_to_string = function
| Duplicated_term te -> Printf.sprintf "Syntax error: Term \"%s\" has already been defined" te
| Binder_expected id -> Printf.sprintf "Syntax error: Unknown binder \"%s\"" id
| Unknown_constant id -> Printf.sprintf "Syntax error: Unknown constant \"%s\"" id
| Unknown_constant_nor_variable id -> Printf.sprintf "Syntax error: Unknown constant or variable \"%s\"" id
| Unknown_constant_nor_type id -> Printf.sprintf "Syntax error: Unknown constant or type \"%s\"" id
| Unknown_type id -> Printf.sprintf "Syntax error: Unknown atomic type \"%s\"" id
| Missing_arg_of_Infix id -> Printf.sprintf "Syntax error: \"%s\" is defined as infix but used here with less than two arguments" id
| No_such_signature s -> Printf.sprintf "Syntax error: Signature id \"%s\" not in the current environment" s
| No_such_lexicon s -> Printf.sprintf "Syntax error: Lexicon id \"%s\" not in the current environment" s
| Dyp_error -> "Dyp: Syntax error"
| Not_associative s -> Printf.sprintf "Syntax error: Operator \"%s\" is not associative but is used without parenthesis" s
| Not_infix s -> Printf.sprintf "Syntax error: Operator \"%s\" is not infix bus is used as infix" s
| Prefix_missing_arg s -> Printf.sprintf "Syntax error: The prefix operator \"%s\" is missing its argument" s
| Infix_missing_first_arg s -> Printf.sprintf "Syntax error: The infix operator \"%s\" is missing its first argument" s
| Infix_missing_second_arg s -> Printf.sprintf "Syntax error: The infix operator \"%s\" is missing its first argument" s
let type_error_to_string = function
| Already_defined_var s ->
......@@ -175,9 +187,13 @@ let lexicon_error_to_string = function
let version_error_to_string = function
| Outdated_version (old_v,current_v) -> Printf.sprintf "You are trying to use an object file that was generated with a former version of the acgc compiler (version %s) while the current version of the compiler is %s" old_v current_v
let warning_to_string w =
let warning_to_string w input_file =
match w with
| Variable_or_constant (s,_,_) -> Printf.sprintf "\"%s\" is a variable here, but is also declared as constant in the signature" s
| Variable_or_constant (s,(start,e)) ->
Printf.sprintf "File \"%s\", %s\nWarning: %s"
input_file
(compute_comment_for_position start e)
(Printf.sprintf "\"%s\" is a variable here, but is also declared as constant in the signature" s)
let error_msg e input_file =
let msg,location_msg =
......@@ -193,18 +209,19 @@ let error_msg e input_file =
| None -> msg
| Some loc -> Printf.sprintf "File \"%s\", %s\n%s" input_file loc msg
(*
let dyp_error lexbuf =
let pos1=Lexing.lexeme_start_p lexbuf in
let pos2=Lexing.lexeme_end_p lexbuf in
match bad_infix_usage () with
| None -> Error (Parse_error (Dyp_error,(pos1,pos2)))
| Some (sym,(s,e)) -> Error (Parse_error (Missing_arg_of_Infix sym,(s,e)))
*)
(*
let emit_warning w input_file =
match w with
| Variable_or_constant (_,pos1,pos2) ->
let msg = warning_to_string w in
| Variable_or_constant (_,(pos1,pos2)) ->
let msg = warning_to_string w input_file in
let line2 = pos2.Lexing.pos_lnum in
let col2 = pos2.Lexing.pos_cnum - pos2.Lexing.pos_bol in
let pos1 = pos1 in
......@@ -216,8 +233,9 @@ let emit_warning w input_file =
else
Printf.sprintf "File \"%s\", from l:%d, c:%d to l:%d,c:%d\nWarning: %s"
input_file line1 col1 line2 col2 msg
let warnings_to_string input_file ws = Utils.string_of_list "\n" (fun w -> emit_warning w input_file) ws
*)
let warnings_to_string input_file ws = Utils.string_of_list "\n" (fun w -> warning_to_string w input_file) ws
let get_loc_error = function
| Parse_error (_,(s,e))
......
......@@ -38,11 +38,17 @@ type parse_error =
| Duplicated_type of string
| Binder_expected of string
| Unknown_constant of string
| Unknown_constant_nor_variable of string
| Unknown_constant_nor_type of string
| Unknown_type of string
| Missing_arg_of_Infix of string
| No_such_signature of string
| No_such_lexicon of string
| Dyp_error
| Not_associative of string
| Not_infix of string
| Prefix_missing_arg of string
| Infix_missing_first_arg of string
| Infix_missing_second_arg of string
(** The types for errors raised by the typechecker. Names should be
explicit *)
......@@ -89,7 +95,7 @@ type error =
(** The type for warnings *)
type warning =
| Variable_or_constant of (string * Lexing.position * Lexing.position)
| Variable_or_constant of (string * (Lexing.position * Lexing.position))
(** The exception that should be raised when an error occur *)
exception Error of error
......@@ -113,10 +119,10 @@ val error_msg : error -> string -> string
(** [dyp_error lexbuf] returns an exception {!Error.Error} so
that it can be caught in a uniform way. [lexbuf] is
used to set correctly the location information of the parse error *)
val dyp_error : Lexing.lexbuf -> exn
(* val dyp_error : Lexing.lexbuf -> exn *)
(** [warnings_to_string filname ws] returns a string describing the
warnings anf their location for the file [filename] *)
warnings and their location for the file [filename] *)
val warnings_to_string : string -> warning list -> string
(** [get_loc_error e] returns the starting and ending position of an
......
......@@ -295,7 +295,7 @@ struct
let behavior_to_string = function
| Abstract_syntax.Default -> ""
| Abstract_syntax.Prefix -> "prefix "
| Abstract_syntax.Infix -> "infix "
| Abstract_syntax.Infix _ -> "infix "
| Abstract_syntax.Binder -> "binder "
let entry_to_string f decl =
......
......@@ -10,7 +10,6 @@
(flags (:standard -w -58))
(modules (:standard db_parser db_lexer \ test db_test))
(libraries
bolt ; external libraries
str ; external libraries
ANSITerminal ; external libraries
utilsLib ; internal library
......@@ -20,7 +19,6 @@
(names test db_test)
(modules test db_test)
(libraries
threads
fmt.tty
utilsLib
datalogLib
......
......@@ -3,7 +3,6 @@
(test
(name test)
(libraries
threads
utilsLib
logic))
......@@ -22,10 +22,20 @@ struct
type location = Lexing.position*Lexing.position
(** The type of the kind of associativity for infix operators *)
type associativity =
| Left
| Right
| NonAss
(** The type of the syntactic behaviour of constants defined in
the signature *)
type syntactic_behavior =
| Default
| Prefix
| Infix
| Default
| Prefix
| Infix of (float * associativity)
(* the float indicates precedence in the total order of infix
operators *)
| Binder
type abstraction =
......
......@@ -25,12 +25,20 @@ sig
(** The type of location in the signature files *)
type location = Lexing.position*Lexing.position
(** The type of the kind of associativity for infix operators *)
type associativity =
| Left
| Right
| NonAss
(** The type of the syntactic behaviour of constants defined in
the signature *)
type syntactic_behavior =
| Default
| Prefix
| Infix
| Infix of (float * associativity)
(* the float indicates precedence in the total order of infix
operators *)
| Binder
......
......@@ -16,7 +16,6 @@
(names typeInference_test)
(modules typeInference_test)
(libraries
threads
fmt.tty
utilsLib
logic))
......
......@@ -106,7 +106,7 @@ module Lambda =
let is_infix id id_to_sym =
match id_to_sym id with
| Abstract_syntax.Infix,_ -> true
| Abstract_syntax.Infix _ ,_ -> true
| _ -> false
let is_prefix id id_to_sym =
......
......@@ -14,7 +14,6 @@
(flags (:standard -w -58))
(modules (:standard \ acg io_test))
(libraries
threads
cairo2
ocf
utilsLib
......@@ -31,7 +30,6 @@
(modules acg)
(flags (:standard -w -58))
(libraries
threads
cairo2
ocf
fmt.tty
......
......@@ -7,7 +7,6 @@
(flags (:standard -w -58))
(modules (:standard \ test_sharedForest test_dependencyManager))
(libraries
bolt ; external libraries
str ; external libraries
ANSITerminal ; external libraries
logs
......@@ -18,7 +17,6 @@
(tests
(names test_sharedForest test_dependencyManager)
(libraries
threads
fmt.tty
utilsLib)
(modules test_sharedForest test_dependencyManager)
......
......@@ -157,7 +157,9 @@ let find_file name dirs =
let (>>) f g = fun x -> f (g x)
(*
let log_iteration log_function s =
List.iter
log_function
(Bolt.Utils.split "\n" s)
*)
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment