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