• Sylvain Dailler's avatar
    PA03-013 counterex: Projection function defined after being applied. · b00248b5
    Sylvain Dailler authored
    This patch solves a problem on the order of the generation of new
    declarations by intro_projections_counterexmp. The problem came from
    the combination of Trans.on_tagged_ls and Trans.decl. The former was used
    to know each projection function in advance and the latter would
    introduce new declarations directly at the definition of the decl being
    analysed sometimes using projections functions before they are defined.
    
    This patch makes intro_projections_counterexmp.ml adds declarations only
    at the end of the task. So we are sure that any meta is really defined
    before.
    
    * src/transform/intro_projections_counterexmp.ml
     (introduce_constant): Minor clarification.
     (projections_for_term): Replacing append with proper symbol. Also adding
      already computed list of declaration to the output.
     (introduce_projs): Removing already defined declarations from the set of
      declaration we will add.
     (build_projections_map): The order of elements is irrelevant so
      it is faster to use cons instead of append.
     (meta_transform2): Add declarations created by f at the end of the task.
     (encapsulate): Compose meta_transform2 and introduce_projs.
     (commented meta_transform2): Request for a fold able to do what is
      described.
    b00248b5
Name
Last commit
Last update
bench Loading commit data...
bin Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
modules Loading commit data...
opam Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitattributes Loading commit data...
.gitignore Loading commit data...
.mailmap Loading commit data...
.merlin.in Loading commit data...
AUTHORS Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
check.sh Loading commit data...
configure.in Loading commit data...