1. 18 Mar, 2010 7 commits
  2. 17 Mar, 2010 18 commits
  3. 16 Mar, 2010 15 commits
    • Andrei Paskevich's avatar
      "I want to believe" commit. · f0218f41
      Andrei Paskevich authored
      Not only Theory, but also Task and Transformation 
      do not need to depend on environment. Moreover,
      we don't have to track the clone history in tasks.
      The only thing we need to do, is to provide three
      registration functions in Driver, namely:
        val register_transform : string -> (unit -> task_t) -> unit
        val register_transform_env : string -> (env -> task_t) -> unit
        val register_transform_clone : string -> (env -> clone -> task_t) -> unit
      and then another three for task_list_t.
      Then any particular transformation that is going to depend
      on environment or clone_history, must register itself via
      the appropriate registration function. It will be the
      responsibility of Driver to recreate the transformation
      for every new environment and/or clone history. It will
      be easy, given that both [env] and [clone] are physically
      comparable and provide a unique tag.
      Thus, the generic interface provided by Transform can be
      completely independent on [env] and [clone].
      This commit implements the proposed interface of Task
      and moves the environment stuff into a separate module.
    • Francois Bobot's avatar
      ajout de la transformation split_to_cnf qui met en une forme presque cnf. Une... · 5f6f38a8
      Francois Bobot authored
      ajout de la transformation split_to_cnf qui met en une forme presque cnf. Une CNF où on garde la position des négations et implications. L'interet est au moins pour la visualisation. On retrouve (normalement) une cnf simplement en poussant les négations.
    • Andrei Paskevich's avatar
    • Andrei Paskevich's avatar
    • Francois Bobot's avatar
    • Francois Bobot's avatar
    • Francois Bobot's avatar
      alt-ergo.ml : decl_type avec arguments · 2a84a8b6
      Francois Bobot authored
      main.ml : possibilité de mettre specifier plusieurs theories ou buts
      split_goals : ajout d'un argument supplémentaire pour ne selectionner que certains buts.
    • Francois Bobot's avatar
      Theory : Correction de l'exception renvoyé quand une théorie n'est pas trouvé... · 736d3efb
      Francois Bobot authored
      Theory : Correction de l'exception renvoyé quand une théorie n'est pas trouvé par la fonction retrieve.
    • Andrei Paskevich's avatar
      Start the separation of contexts and tasks. · a8f76c2f
      Andrei Paskevich authored
      The proposed architecture is as follows:
      - Decl provides the type of declaration, decl, which is a sum
        of type_decl, logic_decl, ind_decl, and prop_decl. decl is 
        h-consed and does not depent on theory, context or anything else.
      - Theory provides the types of theories and theories under construction.
        A theory is a list of (decl | use | clone) with namespace, and the set
        of known idents. Theories are not h-consed and they do not depend on
        env or task.
      - Task provides the types of environment (env), clone maps (clone), and
        the task itself. It might be interesting to merge Transform with Task.
        An environment stays as it is today. A clone map is a private record 
        with the unique tag and physical equality. A task is essentially what
        context is today:
          task_decl  : decl               (* top declaration *)
          task_prev  : task option        (* the previous context *)
          task_known : (ident, decl) map  (* the set of known symbols *)
          task_clone : clone              (* the clone map *)
          task_env   : env                (* the environment *)
          task_tag   : int                (* the unique tag *)
        Tasks are h-consed. There is a guarantee that task_env and task_clone
        of task and task.task_prev are physically equal.
        Unless there is a good reason to do otherwise, the only way to produce
        a task is by split_goal, which takes a theory (and optionally a number
        of goals in it) and creates a list of tasks. Note that sharing IS LOST
        whenever two goals are separated by a clone instruction. However, the
        declarations will still be shared.
      - Trasformation works on tasks, producing task lists, tasks, and alphas.
      - use_export and clone_export may be allowed on tasks, rebuilding the
        whole task, whenever necessary.
      This commit just adds the Decl module, but does not make anything use it.
    • Francois Bobot's avatar
      ajout de l'option print_debug · 930fb870
      Francois Bobot authored
    • Francois Bobot's avatar
      driver utilise maintenant en interne des context list Transform.t · c9f1ab6b
      Francois Bobot authored
      dans les drivers il n'y a qu'une seul liste de transformations
    • Andrei Paskevich's avatar
      - make the interface to ls_defn more straightforward · 8874bce9
      Andrei Paskevich authored
      - assure generation of new variables on create_ls_defn
    • Francois Bobot's avatar
    • Andrei Paskevich's avatar
      minor · 2278ee78
      Andrei Paskevich authored
    • Andrei Paskevich's avatar
      use Driver instructions in Why3 · 9372d2e5
      Andrei Paskevich authored