Commit 71c0244e authored by POGODALLA Sylvain's avatar POGODALLA Sylvain

jbuild files now include testing that all exe (including test ones) now compile

parent 7d4a6497
; -*-org-*-
* Version 1.3.1
** The acg.opt/acg interpreter
+ Bug fix: constants that were given two interpretations in a lexicon
(only the last one is available) generated two rules in the
corresponding datalog program (hence possibly several parses)
+ Bug fix: when an object constant was the direct interpretation of an
abstract constant, parsing this object constant raised an exception
+ an option -svg filename is added to ./acg and ./acg.opt to allow the
user to provide another name than the default "realize.svg" to the
svg output file.
** Configuration and opam file
+ an option --disable-warning-as-errors to the .configure script in
order to make opam compile without the -warn-error A option.
* Version 1.3.0
** The acg.opt/acg interpreter
+ Colors and link between signature and rendering engines are now
defined in a json configuration file. The option to load the
configuration is -realize.
* Version 1.2
** The acg.opt/acg interpreter
+ Added the generation of a "realize.svg" file when the 'realize'
command is invoked. Colors and link between signature and rendering
engines are hard-coded.
+ An option is added to toggle of the realize.svg file generation
(takes a bit of time)
* Version 1.1
** The acgc.opt/acgc compiler and the acg.opt/acg interpreter:
+ Fixed severe bug that prevented finding some parses and sometimes
caused a Fatal Error
+ Added a control on the compiler version that generated the object
(.acgo) files. The version has to be the same as the current version
of the compiler or of the interpreter that is being used.
** The acgc.opt/acgc compiler:
+ added a "nl_lexicon" keyword that causes the interpretation of any
functional type ("->" or "=>") of the abstract signature to be
interpreted by the intuitionistic arrow "=>" in the object signature.
Accordingly, the interpretation should use "Lambda".
** The acg.opt/acg interpreter:
+ Improved terminal output (colors and formatting)
+ added a "-nc" option to disable colored outputs
+ added a "-npp" option to disable formatting on the output
** The acg emacs mode
+ improved handling of long files
* Version 1.0b
** The acgc.opt/acgc compiler:
+ Now outputs an "file.acgo" file when compilation is successful
+ Can declare a lexicon as the composition of two other lexicons
using the following declaration:
lexicon lex_name = lex_name2 << lex_name1
** The acg.opt/acg interpreter:
+ Can load an acg object file using the command:
load o file.acco;
+ The "analyse" command is deprecated. It is replaced by:
+ A "check" command, prefixed by signatures, that typecheck the
typing assignment of a term
Sig1 Sig2 check term:type;
+ A "realize" command that must be preceded by lexicons and followed
by the type assignment of a term. It checks that the term is well
typed in the abstract signatures of the lexicons and compute its
realizations through the lexicons.
Lex1 Lex2 realize term:type;
+ A "parse" command has been added. It must be preceded with the name
of a lexicon and it returns the antecedent by this lexicon of the input
term with respect to some distinguished (atomic) type:
Lex parse object_term:distinguished_type;
+ A "query" command has been added. It follows the "parse" command
syntax and it outputs the associated query and associated extensional
database.
Lex query object_term:distinguished_type;
+ A "idb" command has been added. It must be preceded with the name of
a lexicon and it returns the intensional database associated with
the lexicon
Lex idb;
** Current limitation:
+ Only parse images of atomic types
+ The result of parsing with non-linear lexicons is unspecified yet
This diff is collapsed.
{
(* open Db_parser *)
open Db_parser
}
let newline = ('\010' | '\013' | "\013\010")
......
......@@ -20,7 +20,7 @@
%type < Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t > rule
%type < Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t -> Datalog_AbstractSyntax.AbstractSyntax.Proto_Program.t > program
%type < (Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table) -> (Datalog_AbstractSyntax.AbstractSyntax.Predicate.predicate * Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table) > query
%type < (Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table*IdGenerator.IntIdGen.t) -> (Datalog_AbstractSyntax.AbstractSyntax.Rule.rule list*Datalog_AbstractSyntax.ConstGen.Table.table*IdGenerator.IntIdGen.t) > extensional_facts
%type < (Datalog_AbstractSyntax.AbstractSyntax.Predicate.PredIdTable.table * Datalog_AbstractSyntax.ConstGen.Table.table*UtilsLib.IdGenerator.IntIdGen.t) -> (Datalog_AbstractSyntax.AbstractSyntax.Rule.rule list*Datalog_AbstractSyntax.ConstGen.Table.table*UtilsLib.IdGenerator.IntIdGen.t) > extensional_facts
%%
......
......@@ -29,10 +29,10 @@ let parse_file query edb filename =
open_in fullname in
let lexbuf = Lexing.from_channel in_ch in
LOG "Parsing \"%s\"..." filename LEVEL INFO;
let prog=Db_parser.program Db_lexer.lexer lexbuf AbstractSyntax.Proto_Program.empty in
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 ;
Utils.log_iteration
UtilsLib.Utils.log_iteration
(fun s -> LOG s LEVEL DEBUG)
(AbstractSyntax.Predicate.PredIdTable.to_string prog.AbstractSyntax.Proto_Program.pred_table);
let sep=String.make 15 '*' in
......@@ -55,11 +55,11 @@ let parse_file query edb filename =
| Some edb_filename ->
LOG "I found an edb file to parse." LEVEL DEBUG ;
let edb_in_ch =
let edb_fullname = Utils.find_file edb_filename [""] in
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;
let to_be_added=Db_parser.extensional_facts Db_lexer.lexer edb_lexbuf Datalog.Program.(program.pred_table,program.const_table,program.rule_id_gen) in
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;
Datalog.Program.add_e_facts program to_be_added in
let derived_facts,derivations = Datalog.Program.seminaive program in
......@@ -72,7 +72,7 @@ let parse_file query edb filename =
| None ->
None,program.Datalog.Program.pred_table,program.Datalog.Program.const_table
| Some s ->
let q,t1,t2=Db_parser.query Db_lexer.lexer (Lexing.from_string s) Datalog.Program.(program.pred_table,program.const_table) in
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
......
......@@ -3,7 +3,7 @@
(jbuild_version 1)
(ocamllex (db_lexer))
(ocamlyacc (dp_parser))
(ocamlyacc (db_parser))
;; This stanza declares the DatalogLib
(library
......@@ -12,7 +12,7 @@
((action (system "${bin:camlp4} -parser o -parser op -printer a -loc loc ${lib:bolt:bolt_pp.cmo} -level NONE ${<}" ))
(datalog unionFind))
))
(modules (:standard db_lexer db_parser \ test db_test))
(modules (:standard db_parser db_lexer \ test db_test))
(libraries (bolt ; external libraries
str ; external libraries
ANSITerminal ; external libraries
......@@ -26,7 +26,7 @@
((action (system "${bin:camlp4} -parser o -parser op -printer a -loc loc ${lib:bolt:bolt_pp.cmo} -level NONE ${<}" ))
(db_test))
))
(libraries (
(libraries (threads
utilsLib
datalogLib))))
......
;; -*-lisp-*-
(jbuild_version 1)
(executable
((name test)
(libraries (threads
utilsLib
logic))))
(alias
((name testbuild)
(deps (test.exe))))
......@@ -5,6 +5,7 @@
;; This declares the Logic libreary
(library
((name logic)
(modules (:standard \ typeInference_test type_inference type_inference_test))
(preprocess (per_module
((action (system "${bin:camlp4} -parser o -parser op -printer a -loc loc ${lib:bolt:bolt_pp.cmo} -level NONE ${<}" ))
(typeInference varUnionFind))
......@@ -13,3 +14,13 @@
ANSITerminal ; external library
utilsLib ; internal library
))))
(executables
((names (typeInference_test))
(modules (typeInference_test))
(libraries (threads
utilsLib
logic))))
(alias
((name testbuild)
(deps (typeInference_test.exe))))
open UtilsLib
open TypeInference
open Lambda.Lambda
open Logic.TypeInference
open Logic.Lambda.Lambda
......
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