Commit graph

58 commits

Author SHA1 Message Date
Gwenaël Delaval
2f18926bf4 Clean up documentation comments 2017-03-03 11:41:57 +01:00
Nicolas Berthier
14a7b67a70 New option to force abstraction of infinite-domain state variables in ctrln export
Also add an option to silence related warnings
2015-09-18 14:11:04 +02:00
Nicolas Berthier
2d874f8070 New option to silence warnings about untranslatable constructs 2015-09-18 13:59:33 +02:00
Nicolas Berthier
be21bf31d8 Insertion of call to controller(s) when exporting to Controllable-Nbac node.
To enable recovery of parameter and output ordering by `ctrl2ept', the
Controllable-Nbac generation procedure now declares a new module
dedicated to the encapsulation of the controller functions yet to be
synthesized.

Handling of type declarations are probably buggy.
2014-10-28 16:43:13 +01:00
Nicolas Berthier
99ab12aa13 Fixed warnings. 2014-03-18 11:01:56 +01:00
Nicolas Berthier
10bdab4dc6 Exclusively use ocamlfind; source documentation generation.
- Stripped portions of `myocamlbuild{,_config}.ml' that seem useless
  when `-use-ocamlfind' is passed to ocamlbuild.

- Added some code in `myocamlbuild_config.ml' to be able to generate
  documentation by merging interface and implementation files.
2013-11-08 15:50:36 +01:00
Gwenal Delaval
ce2e2bdcd0 Added -nbvars option for performance evaluation 2012-11-26 10:05:20 +01:00
Gwenaël Delaval
ef536f412d Added option -nosink (CS optimisation)
The -nosink option suppress the sink state of sigali equations.

This optimizes the controller synthesis, but work only
when the synthesis objective instantaneoulsy depends only
on the current state (and not on current inputs).
2012-11-23 12:23:17 +01:00
Gwenaël Delaval
ef00823cf7 Added Marc as co-author 2012-06-29 01:43:15 +02:00
Gwenaël Delaval
58086190eb Headers and license file for GPL
Headers for every source file (excluding examples), mentioning
authors, copyright and license (GPL)

COPYING file with GPLv3 content.
2012-06-27 18:14:29 +02:00
Cédric Pasteur
8815a2cd03 Better handling of clocks in memalloc
- We can do a better allocation if we take into
account 'when' in extvalues 
(test/good/memalloc_clocks.ept shows the
improvement)
- Fixed a bug with memalloc on records: if we 
translate:
o = { a with .f = u }
to
o = a; o.f = u
then we cannot share u and o.f
2012-06-20 09:17:13 +02:00
Adrien Guatto
e05f3732a0 Timing framework. 2012-03-07 17:48:08 +01:00
Adrien Guatto
76ae2f4518 Loop unrolling. 2012-02-08 16:16:41 +01:00
Adrien Guatto
cad8a0149f Option to perform type inference on all types 2012-01-23 13:36:24 +01:00
Adrien Guatto
1b73f3444e Clock before dumping .epci 2011-11-24 11:41:11 +01:00
Léonard Gérard
fdab1ac55c Strict-SSA option to switch array encoding. 2011-11-21 03:26:26 +01:00
Léonard Gérard
76109b553a Add -O option to enable optims. 2011-11-02 17:23:23 +01:00
Léonard Gérard
33021aaa90 Print stateful in heptagon.
Conflicts:

	compiler/heptagon/hept_printer.ml
2011-11-02 13:15:33 +01:00
Léonard Gérard
ffe2b23a82 new sheduler by default 2011-10-23 17:42:26 +02:00
Cédric Pasteur
4d912e9349 Added more options for memalloc
There is now three options for memory allocation:
  - -only-linear activates only the linear 
annotations (with typing and code generation)
  - -only-memalloc does only memory allocation
  - -memalloc does both

When linear typing is not activated, linearity 
annotations are ignored (the signature in the .epi
does not contain the annotations)
2011-09-09 16:05:44 +02:00
Cédric Pasteur
8cc879be7a Generate code from interface (.epi) files
It includes the definition of types, constants
and prototypes defined in the interface.
2011-09-06 11:55:06 +02:00
Cédric Pasteur
379f509dfc Added typing of signatures
This fixes a bug where mapfold would insert 
untyped constants in the code.
2011-09-05 15:33:31 +02:00
Gwenaël Delaval
c57b71b6aa Merge branch 'bzr' into decade
- Added Boolean module (enum types to boolean vectors)
- Added Hept_clocking analysis, called before Boolean
- Added z3z target from minils (sigali format)
- Bug corrections in Normalize, Normalize_mem

Conflicts:
	compiler/heptagon/analysis/typing.ml
	compiler/heptagon/heptagon.ml
	compiler/heptagon/parsing/hept_parser.mly
	compiler/heptagon/parsing/hept_parsetree.ml
	compiler/heptagon/parsing/hept_scoping.ml
	compiler/main/hept2mls.ml
	compiler/main/heptc.ml
	compiler/main/mls2seq.ml
	compiler/minils/minils.ml
	compiler/minils/transformations/normalize_mem.ml
	test/check
2011-08-04 13:37:33 +02:00
Cédric Pasteur
1ea4290f9e Added scheduler that tries to minimize interferences 2011-05-25 09:12:15 +02:00
Cédric Pasteur
9a7f9254d2 Added memalloc pass to the compiler 2011-05-25 09:12:11 +02:00
Gwenal Delaval
acad16b98a Graphical simulator hepts
Added graphical simulator hepts

Added option -hepts to the compiler: this option formats the output of the simulation loop
to fit with hepts (currently working only on C target code). Typically, suppresses all
"decoration" output, like input or output names, and prints output on single lines.

Currently not implemented in hepts: array types.

Usage: to simulate the node Modulename.f:

heptc -target c -s f -hepts modulename.ept
gcc modulename_c/*.c -o ./f_sim
hepts -mod Modulename -node f -exec ./f_sim
2011-05-12 10:08:13 +02:00
Gwenal Delaval
4e267d82c6 Boolean transformation pass (translate every enumeration type to boolean tuples) 2011-04-20 12:28:37 +02:00
Cédric Pasteur
57bc9f210b Added a generic onfiguration for backends
Each backend gives a function used to 
enable/disable passes, executed before the
beginning of the compilation
2011-04-14 13:53:30 +02:00
Léonard Gérard
8f4411e145 Recursives Qualnames.
In order to have a correct handling of inner classes in Java, and to prepare for modules inside modules.
2011-02-07 14:24:17 +01:00
Léonard Gérard
0768babab7 Removed brocken and useless mlsc, cleaned heptc. 2011-01-07 17:30:04 +01:00
Léonard Gérard
e174151d37 Unclutter ident printing. 2010-12-15 11:27:19 +01:00
Léonard Gérard
2ae809c971 Fresh vars, and ident refactoring.
Idents.enter_node should be called when entering a node, it is done automagically by the mapfold unless you call directly Hept_mapfold.node_dec.
2010-12-15 11:26:29 +01:00
Gwenal Delaval
b7cba3315a Compiler option -nocaus
Added a compiler option de-activating causality analysis
2010-12-08 17:31:16 +01:00
Cédric Pasteur
0bb84532b9 Added a new static scoping pass
This pass transforms exps that should be static 
to Econst se. The regular scoping then only has
to check this case.

The conversion is done in a single traversal of
the AST (unlike the old solution).
2010-11-20 17:39:24 +01:00
Adrien Guatto
6ff8ed993f Switched back to plain strings for some compiler options.
To be consistent or to be convenient, that is the question.
2010-10-04 00:35:12 +02:00
Adrien Guatto
4044d8a0a2 Automata minimization. 2010-09-30 21:52:32 +02:00
Adrien Guatto
a4c3d9e856 Relevant command-line options are now stored as qualnames. 2010-09-30 21:40:04 +02:00
Cédric Pasteur
db732621a1 Re enabled iterator fusion
Added an option to enable it (off by default)
2010-09-15 09:53:20 +02:00
Cédric Pasteur
df12e081ae Refactored Misc
Created two new files: 
 - utilities/global/compiler_options.ml: contains
 the options that can be set using the cli
 - utilities/global/errors.ml: contains global
 errors definition

Misc now only contains helper functions that have 
nothing to do with the ast or the compiler.
2010-09-15 09:38:52 +02:00
Cédric Pasteur
cc039ac42d Make heptc compile 2010-09-10 14:29:13 +02:00
Léonard Gérard
a54e570d0f Hept Scoping should be ok and documented,
Hept Parsing too,
all the reset to review carefully,
Typing to cut from all the scoping.
2010-09-09 19:48:20 +02:00
Léonard Gérard
418b961293 Small fixes to the compilation processes.
*Locations should be pretty damn good now.
*Mlsc is up to date, still need a scoping pass (to be posted soon)
2010-08-02 16:31:57 +02:00
Cédric Pasteur
2e44402b03 Two fixes in heptc
- Add the directory of the file as an include
- write interfaces with uncapitalized filenames,
as expected by modules.
2010-07-27 14:00:15 +02:00
Adrien Guatto
7f91ffab53 Output MiniLS code before clocking when in verbose mode. 2010-07-22 11:12:58 +02:00
Léonard Gérard
5e737d0094 location change. Heptc works with menhir. 2010-07-21 15:15:57 +02:00
Adrien Guatto
d75f4f8901 Added an option for global inlining (-flatten). 2010-07-19 13:20:11 +02:00
Adrien Guatto
1d6df4ecb2 Inlining pass added. Use with -inline. 2010-07-19 12:02:29 +02:00
Léonard Gérard
c657ce8ecb Schedule with the iterator and eqs/var_decs added in mapfold. 2010-07-14 03:45:38 +02:00
Cédric Pasteur
ee767064b1 Instantiation of parametrized nodes (v2)
- Many changes to make Hept2mls, mls2obc, etc
compile with the api changes
- Added Callgraph_mapfold: starting from a main
program, generates the list of instances of each
node necessary and creates them.
- Mls2seq deals with giving to the code generators
the correct source (mls or obc, wit or without
static parameters)

It is now possible to use parametrized nodes that 
are defined in other files. For that to work, the 
first file has to be compiled to an object file:
	heptc -c mylib.ept
which creates a mylib.epo file. Compiling the main
file will then generate all the instances of 
parametrized nodes from the lib (only the called 
nodes will be compiled, but all the nodes in the 
main file are compiled).
2010-07-13 14:03:39 +02:00
Cédric Pasteur
2fd0860ba8 Renamed Scoping and Parsetree 2010-07-08 15:19:04 +02:00