• 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.