GitLab

Theory : Correction de l'exception renvoyé quand une théorie n'est pas trouvé par la fonction retrieve.

- assure generation of new variables on create_ls_defn

provide ns_find_prop and ns_find_fmla for convenience

to use proposition names as propositional variables

- unify Lfunction and Lpredicate (mucho bettar)
- separation of prop and fmla
- making prop and tvsymbol private aliases of ident

without changing their order - NOT a topological sort

- copy the code of Pretty to Why3 to prepare it for Driver
- move goal_of_ctxt to Transform, where it belongs 
- comment out the unused "extract_goals" in Transform
- comment out the debugging printing in Theory, use Pretty
- in use_export, put the Duse declaration after the copied
  declarations, not before

Mise à jour de transform, inlining,flatten,... cependant anomalie car un use peut être ajouté par add_decl...

- split clone code between contexts and theories

- add [Dclone] declarations after cloned decls

- account for the used theories in [ctxt_known]
  (the hash-consed [Duse] declaration is referenced)

- provide use and clone for contexts with a distinct semantics:

    Context.use_export ctxt th :
        Copies the contents of [th] and its dependencies
        into [ctxt]. The [Duse] declarations are erased
        from the list of decls, but keeped in [ctxt_known],
        so that theories are not copied twice. Useful to
        build flat contexts.

    Context.clone_export ctxt th :
        Clones the contents of [th] into [ctxt]. Dependencies
        of [th] are copied, too. Erases the [Duse] declarations,
        but keeps them in [ctxt_known], so that theories are not
        copied twice. Useful to build flat contexts.

    Theory.use_export uc th :
        Marks the dependency on [th]. [Duse th] is added to [uc],
        unless [th] is already used.

    Theory.clone_export uc th :
        Clones the contents of [th] into [uc]. The dependencies
        of [th] become dependencies of [uc]. [Duse] declarations
        are added, when a theory is used for the first time.